diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-08-02 16:20:45 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-02 16:20:45 -0700 |
| commit | 5001fa069ab42134333244b3f27c852724cea3e2 (patch) | |
| tree | c03b1730016a03094064b01311d5a529d9e00641 /test/regress | |
| parent | 902262c421e52405204b3a95310c8414cc51a5c5 (diff) | |
Update CaDiCaL to version 1.0.3. (#3137)
* Removes incremental API check (#3011)
* Fixes toSatValueLit to use the new semantics of CaDiCaL's val()
Fixes #3011
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bv/eager-inc-cadical.smt2 | 27 |
2 files changed, 28 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9a1e5d6dc..df553b8bd 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -250,6 +250,7 @@ set(regress_0_tests regress0/bv/core/slice-20.smt regress0/bv/divtest_2_5.smt2 regress0/bv/divtest_2_6.smt2 + regress0/bv/eager-inc-cadical.smt2 regress0/bv/eager-inc-cryptominisat.smt2 regress0/bv/eager-force-logic.smt2 regress0/bv/fuzz01.smt diff --git a/test/regress/regress0/bv/eager-inc-cadical.smt2 b/test/regress/regress0/bv/eager-inc-cadical.smt2 new file mode 100644 index 000000000..01840dffa --- /dev/null +++ b/test/regress/regress0/bv/eager-inc-cadical.smt2 @@ -0,0 +1,27 @@ +; REQUIRES: cadical +; COMMAND-LINE: --incremental --bv-sat-solver=cadical --bitblast=eager +(set-logic QF_BV) +(set-option :incremental true) +(declare-fun a () (_ BitVec 16)) +(declare-fun b () (_ BitVec 16)) +(declare-fun c () (_ BitVec 16)) + +(assert (bvult a (bvadd b c))) +(set-info :status sat) +(check-sat) + +(push 1) +(assert (bvult c b)) +(set-info :status sat) +(check-sat) + + +(push 1) +(assert (bvugt c b)) +(set-info :status unsat) +(check-sat) +(pop 2) + +(set-info :status sat) +(check-sat) +(exit) |