EBMC on HWMCC08

Results of running ebmc in bounded mode over the HWMCC08 AIG benchmarks.
SAT benchmarks are checked at the published counterexample bound; UNSAT benchmarks are smoke-tested by confirming that ebmc does not report a counterexample at bound 2.
Generated 2026-09-07 20:10:25 UTC · ebmc 6.0 (20fa672)

645benchmarks

433passed

60failed

152skipped

Benchmark	Expected	Bound	Observed	Result
139442p0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
139442p0neg	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
139442p1	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
139442p1neg	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
139442p22	sat at 4	4	counterexample at bound 4	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
139442p23	sat at 4	4	counterexample at bound 4	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
139442p24	sat at 4	4	counterexample at bound 4	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
139442p5	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
139442p5neg	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
139442p6	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139442p6neg	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
139443p0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
139443p0neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139443p1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139443p1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139443p22	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139443p23	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139443p24	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139443p5	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139443p5neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139443p6	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139443p6neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139444p0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
139444p0neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139444p1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139444p1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139444p22	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139444p23	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139444p24	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139444p5	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139444p5neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139444p6	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139444p6neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139452p0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
139452p0neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139452p1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139452p1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139452p22	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139452p23	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139452p24	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139452p5	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139452p5neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139452p6	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139452p6neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139453p0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
139453p0neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139453p1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139453p1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139453p22	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139453p23	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139453p24	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139453p5	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139453p5neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139453p6	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139453p6neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139454p0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
139454p0neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139454p1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139454p1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139454p22	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139454p23	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139454p24	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139454p5	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139454p5neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139454p6	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139454p6neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139462p0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
139462p0neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139462p1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139462p1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139462p22	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139462p23	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139462p24	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139462p5	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139462p5neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139462p6	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139462p6neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139463p0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
139463p0neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139463p1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139463p1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139463p22	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139463p23	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139463p24	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139463p5	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139463p5neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139463p6	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139463p6neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139464p0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
139464p0neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139464p1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139464p1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139464p22	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139464p23	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139464p24	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139464p5	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139464p5neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139464p6	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
139464p6neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
abp4p2ff	sat at 17	17	counterexample at bound 17	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
abp4p2tt	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
abp4pold	sat at 17	17	counterexample at bound 17	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
abp4ptimo	sat at 20	20	counterexample at bound 20	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
abp4ptimoneg	sat at 20	20	counterexample at bound 20	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bc57sensorsp0	sat at 104	104	counterexample at bound 104	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bc57sensorsp0neg	sat at 104	104	counterexample at bound 104	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bc57sensorsp1	sat at 104	104	counterexample at bound 104	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bc57sensorsp1neg	sat at 104	104	counterexample at bound 104	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bc57sensorsp2	sat at 104	104	counterexample at bound 104	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bc57sensorsp2neg	sat at 104	104	counterexample at bound 104	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bc57sensorsp3	sat at 104	104	counterexample at bound 104	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08amba2g1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba2g3f1	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08amba2g3f2	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08amba2g3f3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba2g4f1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
bj08amba2g4f2	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08amba2g4f3	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
bj08amba2g5	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba2g62	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba2g82	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba3g1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba3g3	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
bj08amba3g5	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba3g62	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba3g82	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba4g1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba4g5	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba4g82	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba5g62	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08amba5g82	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08aut1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08aut5	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08aut62	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08aut82	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bj08autg3f1	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08autg3f2	sat at 1	1	counterexample at bound 1	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08autg3f3	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08goodbakerycyclef1	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08goodbakerycyclef10	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08goodbakerycyclef7	sat at 1	1	counterexample at bound 1	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08vendingcycle	sat at 4	4	counterexample at bound 4	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08vsar12	sat at 1	1	counterexample at bound 1	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08vsar16	sat at 1	1	counterexample at bound 1	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08vsar6	sat at 1	1	counterexample at bound 1	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bj08vsar8	sat at 1	1	counterexample at bound 1	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
bjrb07amba10andenv	T	-	unsupported expected result "T"	unknown expectation
no log captured
bjrb07amba1andenv	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bjrb07amba2andenv	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bjrb07amba3andenv	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bjrb07amba4andenv	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bjrb07amba5andenv	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bjrb07amba6andenv	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bjrb07amba7andenv	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
bjrb07amba9andenv	T	-	unsupported expected result "T"	unknown expectation
no log captured
brpp1	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
brpp1neg	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
brpptimo	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
brpptimoneg	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
brpptimonegnv	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
cmudme1	T	-	unsupported expected result "T"	unknown expectation
no log captured
cmudme2	T	-	unsupported expected result "T"	unknown expectation
no log captured
cmugigamax	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
cmuperiodic	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
counterp0	sat at 9	9	counterexample at bound 9	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
counterp0neg	sat at 9	9	counterexample at bound 9	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
csmacdp0	sat at 7	7	counterexample at bound 7	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
csmacdp0neg	sat at 7	7	counterexample at bound 7	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
csmacdp2	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
csmacdp2neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
dme3p1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
dme3p1neg	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
dme3ptimo	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
dme3ptimoneg	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
dme3ptimonegnv	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
dme4p1	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
dme4p1neg	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
dme4ptimo	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
dme4ptimoneg	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
dme4ptimonegnv	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
dme5p1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
dme5p1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
dme5ptimo	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
dme5ptimoneg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
dme5ptimonegnv	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
dme6p1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
dme6p1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
dme6ptimo	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
dme6ptimoneg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
dme6ptimonegnv	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
eijkbs1512	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkbs3271	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkbs3330	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkbs3384	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkbs4863	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkbs6669	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS1196	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS1238	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS1423	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS208	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS208c	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS208o	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS298	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS344	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS349	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS382	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS386	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS420	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS444	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS510	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS526	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS5378	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS641	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS713	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS820	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS832	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS838	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
eijkS953	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
intel001	uns	-	benchmark file missing	missing
no log captured
intel002	uns	-	benchmark file missing	missing
no log captured
intel003	uns	-	benchmark file missing	missing
no log captured
intel004	uns	-	benchmark file missing	missing
no log captured
intel005	?	-	benchmark file missing	missing
no log captured
intel006	?	-	benchmark file missing	missing
no log captured
intel007	T	-	benchmark file missing	missing
no log captured
intel009	?	-	benchmark file missing	missing
no log captured
intel010	T	-	benchmark file missing	missing
no log captured
intel011	T	-	benchmark file missing	missing
no log captured
intel012	?	-	benchmark file missing	missing
no log captured
intel013	T	-	benchmark file missing	missing
no log captured
intel014	?	-	benchmark file missing	missing
no log captured
intel015	T	-	benchmark file missing	missing
no log captured
intel016	?	-	benchmark file missing	missing
no log captured
intel017	?	-	benchmark file missing	missing
no log captured
intel018	T	-	benchmark file missing	missing
no log captured
intel019	T	-	benchmark file missing	missing
no log captured
intel020	T	-	benchmark file missing	missing
no log captured
intel021	T	-	benchmark file missing	missing
no log captured
intel022	T	-	benchmark file missing	missing
no log captured
intel023	T	-	benchmark file missing	missing
no log captured
intel024	T	-	benchmark file missing	missing
no log captured
intel025	T	-	benchmark file missing	missing
no log captured
intel026	?	-	benchmark file missing	missing
no log captured
intel027	?	-	benchmark file missing	missing
no log captured
intel028	?	-	benchmark file missing	missing
no log captured
intel029	T	-	benchmark file missing	missing
no log captured
intel030	T	-	benchmark file missing	missing
no log captured
intel031	?	-	benchmark file missing	missing
no log captured
intel032	T	-	benchmark file missing	missing
no log captured
intel033	?	-	benchmark file missing	missing
no log captured
intel034	?	-	benchmark file missing	missing
no log captured
intel035	?	-	benchmark file missing	missing
no log captured
intel036	?	-	benchmark file missing	missing
no log captured
intel037	T	-	benchmark file missing	missing
no log captured
intel038	T	-	benchmark file missing	missing
no log captured
intel039	T	-	benchmark file missing	missing
no log captured
intel040	T	-	benchmark file missing	missing
no log captured
intel041	T	-	benchmark file missing	missing
no log captured
intel042	T	-	benchmark file missing	missing
no log captured
intel043	?	-	benchmark file missing	missing
no log captured
intel044	T	-	benchmark file missing	missing
no log captured
intel045	T	-	benchmark file missing	missing
no log captured
intel046	T	-	benchmark file missing	missing
no log captured
intel047	T	-	benchmark file missing	missing
no log captured
intel048	T	-	benchmark file missing	missing
no log captured
intel049	T	-	benchmark file missing	missing
no log captured
intel052	uns	-	benchmark file missing	missing
no log captured
intel054	T	-	benchmark file missing	missing
no log captured
intel055	T	-	benchmark file missing	missing
no log captured
intel056	T	-	benchmark file missing	missing
no log captured
intel057	T	-	benchmark file missing	missing
no log captured
intel059	T	-	benchmark file missing	missing
no log captured
intel062	T	-	benchmark file missing	missing
no log captured
intel063	uns	-	benchmark file missing	missing
no log captured
intel064	T	-	benchmark file missing	missing
no log captured
intel065	T	-	benchmark file missing	missing
no log captured
intel066	T	-	benchmark file missing	missing
no log captured
intel067	T	-	benchmark file missing	missing
no log captured
irstdme4	T	-	unsupported expected result "T"	unknown expectation
no log captured
irstdme5	T	-	unsupported expected result "T"	unknown expectation
no log captured
irstdme6	T	-	unsupported expected result "T"	unknown expectation
no log captured
kenflashp01	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenflashp02	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
kenflashp03	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenflashp04	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenflashp05	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenflashp06	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenflashp07	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenflashp08	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenflashp09	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenflashp10	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenflashp11	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenflashp12	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
kenflashp13	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenflashp14	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenoopp1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
kenoopp2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
mutexp0	sat at 7	7	counterexample at bound 7	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
mutexp0neg	sat at 7	7	counterexample at bound 7	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
neclabakery001	T	-	unsupported expected result "T"	unknown expectation
no log captured
neclaftp1001	?	-	unsupported expected result "?"	unknown expectation
no log captured
neclaftp1002	?	-	unsupported expected result "?"	unknown expectation
no log captured
neclaftp2001	?	-	unsupported expected result "?"	unknown expectation
no log captured
neclaftp2002	?	-	unsupported expected result "?"	unknown expectation
no log captured
neclaftp3001	sat at 13	13	counterexample at bound 13	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
neclaftp3002	sat at 15	15	counterexample at bound 15	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
neclaftp4001	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
neclaftp4002	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
neclaftp5001	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
neclaftp5002	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
neclatcas1a001	S6	-	unsupported expected result "S6"	unknown expectation
no log captured
neclatcasall001	S6	-	unsupported expected result "S6"	unknown expectation
no log captured
nusmvbrp	T	-	unsupported expected result "T"	unknown expectation
no log captured
nusmvdme116	T	-	unsupported expected result "T"	unknown expectation
no log captured
nusmvdme216	T	-	unsupported expected result "T"	unknown expectation
no log captured
nusmvguidancep1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvguidancep2	?	-	unsupported expected result "?"	unknown expectation
no log captured
nusmvguidancep4	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvguidancep5	T	-	unsupported expected result "T"	unknown expectation
no log captured
nusmvguidancep6	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvguidancep7	T	-	unsupported expected result "T"	unknown expectation
no log captured
nusmvguidancep8	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvguidancep9	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvqueue	T	-	unsupported expected result "T"	unknown expectation
no log captured
nusmvreactorp1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvreactorp2	T	-	unsupported expected result "T"	unknown expectation
no log captured
nusmvreactorp3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvreactorp4	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvreactorp5	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvreactorp6	T	-	unsupported expected result "T"	unknown expectation
no log captured
nusmvsyncarb10p2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvsyncarb5p2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvtcasp1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
nusmvtcasp2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvtcasp3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvtcasp4	sat at 15	15	counterexample at bound 15	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
nusmvtcasp5	sat at 24	24	counterexample at bound 24	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
nusmvtcasp6	sat at 17	17	counterexample at bound 17	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
nusmvtcastp1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
nusmvtcastp2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvtcastp3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
nusmvtcastp4	sat at 15	15	counterexample at bound 15	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
nusmvtcastp5	sat at 24	24	counterexample at bound 24	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
nusmvtcastp6	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
pcip1	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pcip1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
pcipFtimo	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pciptimo	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
pciptimoneg	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtpmsam2901	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsarbiter	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsblackjack	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsbufferalloc	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmscoherence	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmseisenberg	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsfpmult	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsgigamax	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsgoodbakery	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsheap	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsmatrix	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsmiim	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsns2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsns3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmspalu	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsretherrtf	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsrethersqo	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsrotate32	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmss1269b	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmssfeistel	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmssyncarb	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmstimeout	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmstwo	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsusbphy	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsvending	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtpmsviper	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtpmsvsa16a	S6	-	unsupported expected result "S6"	unknown expectation
no log captured
pdtpmsvsar	S6	-	unsupported expected result "S6"	unknown expectation
no log captured
pdtvisbakery0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisbakery1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisbakery2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisbakery3	sat at 1	1	counterexample at bound 1	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvisblackjack0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisblackjack1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisblackjack2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisblackjack3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisblackjack4	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisbpb0	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvisbpb1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisbufferalloc	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtviscoherence0	sat at 4	4	counterexample at bound 4	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtviscoherence1	sat at 12	12	counterexample at bound 12	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtviscoherence2	sat at 4	4	counterexample at bound 4	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtviscoherence3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtviscoherence4	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtviscoherence5	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtviseisenberg0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtviseisenberg1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtviseisenberg2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisfifos	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvisgigamax0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisgigamax1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisgigamax2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisgigamax3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisgigamax4	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisgigamax5	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisgoodbakery0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisgoodbakery1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisgoodbakery2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisgray0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisgray1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap00	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap01	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap02	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap03	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap04	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap05	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap06	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap07	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap08	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap09	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap10	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap11	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisheap12	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvishuffman0	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvishuffman1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvishuffman2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvishuffman3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvishuffman4	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvishuffman5	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvishuffman6	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvishuffman7	sat at 5	5	counterexample at bound 5	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvismiim0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvismiim1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvismiim2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvismiim3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvismiim4	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvismiim5	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvismiim6	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisminmax0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisminmax1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisminmax2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisminmaxr0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisminmaxr1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisminmaxr2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisminmaxr3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns2p0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns2p1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns2p2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns2p3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns2p4	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
pdtvisns2p5	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns2p6	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns2p7	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns2p8	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns3p00	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvisns3p01	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvisns3p02	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvisns3p03	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvisns3p04	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvisns3p05	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvisns3p06	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvisns3p07	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvisns3p08	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvisns3p09	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvisns3p10	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns3p11	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
pdtvisns3p12	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns3p13	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns3p14	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns3p15	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns3p16	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns3p17	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns3p18	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisns3p19	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvispeterson	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisretherrtf0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisretherrtf1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisretherrtf2	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvisretherrtf3	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvisretherrtf4	sat at 32	32	counterexample at bound 32	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvisrethersqo0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisrethersqo1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisrethersqo2	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
pdtvisrethersqo3	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvisrethersqo4	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvissfeistel	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvissoap0	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvissoap1	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvissoap2	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvistictactoe00	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistictactoe01	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvistictactoe02	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvistictactoe03	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvistictactoe04	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvistictactoe05	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvistictactoe06	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvistictactoe07	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvistictactoe08	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvistictactoe09	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvistictactoe10	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistictactoe11	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistictactoe12	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistictactoe13	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistimeout0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistimeout1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistimeout2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistimeout3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistwo0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistwo1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistwoall0	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistwoall1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvistwoall2	sat at 0	0	counterexample at bound 0	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
pdtvistwoall3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvending00	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvending01	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvending02	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvending03	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvending04	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvending05	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvending06	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvending07	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvending08	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvending09	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvending10	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a00	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a01	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a02	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a03	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a04	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a05	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a06	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a07	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a08	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a09	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a10	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a11	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a12	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a13	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a14	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a15	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a16	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a17	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a18	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a19	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a20	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a21	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a22	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a23	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a24	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a25	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a26	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a27	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsa16a29	T	-	unsupported expected result "T"	unknown expectation
no log captured
pdtvisvsa16a31	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar00	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar01	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar02	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar03	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar04	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar05	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar06	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar07	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar08	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar09	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar10	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar11	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar12	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar13	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar14	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar15	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar16	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar17	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar18	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar19	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar20	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar21	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar22	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar23	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar24	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar25	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar26	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar27	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
pdtvisvsar29	?	-	unsupported expected result "?"	unknown expectation
no log captured
pdtvisvsar31	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
prodcellp0	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
prodcellp0neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
prodcellp1	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
prodcellp1neg	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
prodcellp2	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
prodcellp2neg	sat at 127	127	counterexample at bound 127	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodcellp3	sat at 82	82	counterexample at bound 82	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodcellp3neg	sat at 82	82	counterexample at bound 82	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodcellp4	sat at 82	82	counterexample at bound 82	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodcellp4neg	sat at 82	82	counterexample at bound 82	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodconsp0	sat at 22	22	counterexample at bound 22	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodconsp0neg	sat at 22	22	counterexample at bound 22	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodconsp1	sat at 22	22	counterexample at bound 22	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodconsp1negnv	sat at 22	22	counterexample at bound 22	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodconsp5	sat at 22	22	counterexample at bound 22	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodconsp5neg	sat at 22	22	counterexample at bound 22	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodconspold1	sat at 22	22	counterexample at bound 22	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodconspold3	sat at 22	22	counterexample at bound 22	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
prodconspold4	sat at 22	22	counterexample at bound 22	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
ringp0	sat at 8	8	counterexample at bound 8	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
ringp0neg	sat at 8	8	counterexample at bound 8	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
shortp0	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
shortp0neg	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
srg5ptimo	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
srg5ptimoneg	sat at 2	2	counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
srg5ptimonegnv	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
texasifetch1p1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
texasifetch1p2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
texasifetch1p3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
texasifetch1p4	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
texasifetch1p5	sat at 20	20	counterexample at bound 20	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
texasifetch1p8	sat at 4	4	counterexample at bound 4	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
texasparsesysp1	sat at 9	9	counterexample at bound 9	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
texasparsesysp2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
texasparsesysp3	sat at 8	8	counterexample at bound 8	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
texasparsesysp4	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
texasPImainp01	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
texasPImainp02	sat at 3	3	counterexample at bound 3	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
texasPImainp05	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
texasPImainp08	sat at 9	9	counterexample at bound 9	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
texasPImainp12	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
texasPImainp15	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
texastwoprocp1	sat at 14	14	counterexample at bound 14	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
texastwoprocp2	sat at 15	15	counterexample at bound 15	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
texastwoprocp5	sat at 14	14	counterexample at bound 14	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
vis4arbitp1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
visarbiter	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
visbakery	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
viscoherencep1	sat at 8	8	counterexample at bound 8	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
viscoherencep2	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
viscoherencep3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
viscoherencep5	sat at 5	5	counterexample at bound 5	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
viseisenberg	sat at 20	20	counterexample at bound 20	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
viselevatorp1	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
viselevatorp2	sat at 4	4	counterexample at bound 4	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is SATISFIABLE SAT: path found SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : REFUTED
viselevatorp3	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
visemodel	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
visprodcellp01	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
visprodcellp03	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2
visprodcellp07	sat	-	expected SAT, but no published counterexample length	no reference bound
no log captured
visprodcellp22	uns	2	no counterexample at bound 2	ok
EBMC version 6.0 (20fa672) 64-bit x86_64 linux Generating Decision Problem Using MiniSAT 2.2.1 with simplifier Properties Solving with propositional reduction SAT checker inconsistent: instance is UNSATISFIABLE UNSAT: No path found within bound ** Results: [output0] : PROVED up to bound 2