java-smt

java-smt copied to clipboard

Princess: match error in model evaluation (found in CPAchecker benchmark)

1

LOG: ``` scripts/cpa.sh -heap 13000M -noout -benchmark -stack 50M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop counterexample.export.allowImpreciseCounterexamples=true -setprop cpa.predicate.encodeFloatAs=INTEGER -bmc -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=INTEGER -setprop cpa.loopbound.maxLoopIterations=10 -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/nla-digbench-scaling/freire1_valuebound1.c --------------------------------------------------------------------------------...

kfriedberger

Princess: unexpected formula type "_0[any]" (found in CPAchecker benchmark)

1

LOG: ``` scripts/cpa.sh -heap 13000M -noout -benchmark -stack 50M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop counterexample.export.allowImpreciseCounterexamples=true -setprop cpa.predicate.encodeFloatAs=INTEGER -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/loop-crafted/simple_array_index_value_4.i -------------------------------------------------------------------------------- Running CPAchecker...

kfriedberger

Princess: missing arithmetic atom in interpolation (found in CPAchecker benchmark)

1

LOG: ``` scripts/cpa.sh -heap 13000M -noout -benchmark -stack 50M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop counterexample.export.allowImpreciseCounterexamples=true -setprop cpa.predicate.encodeFloatAs=INTEGER -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/loop-acceleration/diamond_2-2.c -------------------------------------------------------------------------------- Running CPAchecker...

kfriedberger

LOG: ``` scripts/cpa.sh -heap 13000M -noout -benchmark -stack 50M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop counterexample.export.allowImpreciseCounterexamples=true -setprop cpa.predicate.encodeFloatAs=INTEGER -kInduction -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=INTEGER -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/loop-acceleration/array_2-1.i -------------------------------------------------------------------------------- Running CPAchecker...

kfriedberger

see #381 for details

kfriedberger

Following my discussion with @baierd, I'm providing a (somewhat) minimal working example for the bug where re-adding the same constraint twice makes it impossible to query interpolants. **Setup**: add one...

leventeBajczi

support for Mac with M series chips

9

Curious about the timeline to support Mac with Apple M1,2,3?

baoluomeng

Issues with NNF tactic and if-then-else terms

1

Consider the following test: ```java @Test public void testNNF_IfThenElse() throws InterruptedException, SolverException { IntegerFormula ifThenElse = bmgr.ifThenElse(bmgr.makeVariable("a"), imgr.makeVariable("b"), imgr.makeVariable("c")); BooleanFormula atom = imgr.equal(ifThenElse, imgr.makeNumber(1)); BooleanFormula nnf = mgr.applyTactic(atom, Tactic.NNF); assertThatFormula(nnf).isEquisatisfiableTo(atom);...

PhilippWendler

Enable Simplify API for Bitwuzla

1

Bitwuzla supports simplification of formulas via the `simplify()` call. We should enable this in our wrapper for the next update of Bitwuzla.

baierd

Bitwuzla is unusualy slow for FP query based on IEEE conversion

1

Bitwuzla is very slow for the tests in `FloatingPointFormulaManagerTest` based on the `getListOfFloats()` method. We should extract examples and inform the devs of Bitwuzla about this.

baierd