Project

General

Profile

Bug #3500

Hifrog - prop logic: Assertion `clause_in_A || clause_in_B' failed

Added by Karine Even Mendoza about 3 years ago. Updated about 3 years ago.

Status:
Resolved
Priority:
Low
Start date:
08/09/2016
Due date:
% Done:

100%

Estimated time:

Description

Happens when running all the claims at once. When running this benchmarks one claim after another (3 runs instead of 1), then there is no problem
Code example: /hi-bench/main-bench/funfrog_regression/05_McMillan/diskperf.cil_loopfree.c

Output:
; ============================[ Search Statistics ]==============================
; | Conflicts | ORIGINAL | LEARNT | Progress |
; | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
; ===============================================================================
; 0 | 0 0 | 53.660 s | 369.918 MB
SOLVER TIME: 54.877
UNSAT - it holds!
ASSERTION IS TRUE
Start generating interpolants...
  1. Proof graph building begin
  2. Memory used before building the proof: 371.594 MB
  3. (1) Empty clause given in input or generated at preprocessing time: single node proof
  4. Number of nodes: 1 (leaves: 0 - learnt: 0 - derived: 0 - theory: 0)
  5. Maximum, average size of leaves: 0 -nan
  6. Maximum, average size of learnt: 0 -nan
  7. Number of edges: 0
  8. Number of distinct variables in the proof: 0
  9. Memory used after building the proof: 371.941 MB
  10. Proof graph building end
  11. Single interpolant
  12. Using Pudlak for propositional interpolation
    evolcheck: PGInterAux.C:210: opensmt::icolor_t ProofGraph::getClauseColor(const ipartitions_t&, const ipartitions_t&): Assertion `clause_in_A || clause_in_B' failed.
    Aborted (core dumped)

History

#1 Updated by Antti Hyvärinen about 3 years ago

  • Status changed from New to Resolved
  • % Done changed from 0 to 100

Seems to be working now in hi frog / master and opensmt2 / master

Also available in: Atom PDF