java-smt
java-smt copied to clipboard
sosy-lab
JavaSMT - Unified Java API for SMT solvers.
Parsing 2 equal Strings to formulas results in 2 non-equal formulas. It seems like variables are not reused, but created anew with each query. We should ask the Bitwuzla devs...
Bitwuzla (currently available on the branch add_bitwuzla) crashes with a SIGABRT when trying to parse incomplete formulas/queries. We shoud ask the devs to ease this into a non-critical abort that...
Integrating dReal to JavaSMT. Problems with dReal: - dReal does not support UF's - dReal does not support existential quantifier - dReal uses delta-precision, therefore Integer formulas are unsound: -...
I've added two methods to copy a prover to the solver context with an implementation for Z3 including tests. Note: it seems like Z3 supports this only for the base...
It would be nice to clone a full ProverEnvironment with its current stack (it would also be ok if the full SolverContext is cloned). Our use case: We incrementally build...
The [getting started](https://github.com/sosy-lab/java-smt/blob/master/doc/Getting-started.md) guide is outdated and should be updated to the most recent version. Also, we might want to include this in our process in the future. Since the...
The following test fails with Z3: ```java BooleanFormula var1 = bmgr.makeVariable("var1"); BooleanFormula var2 = bmgr.makeVariable("var2"); BooleanFormula var3 = bmgr.makeVariable("var3"); BooleanFormula var4 = bmgr.makeVariable("var4"); assertThat(bmgr.and(bmgr.and(var1, var2), bmgr.and(var3, var4))) .isEqualTo(bmgr.and(var1, var2, var3,...
This issue documents the process and issues of adding Apron as a SMT solver in JavaSMT.
This issue documents the addition of dReal to JavaSMT by @juliusbrehme. Problems are discussed and/or documented here if necassary.
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=CVC4 -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/prodbin-ll.c --------------------------------------------------------------------------------...
