diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-08-28 14:42:51 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-28 16:42:51 -0500 |
commit | 48dfcfd271ff9fa04766e29fb82ba83290da1ad8 (patch) | |
tree | c187227cf376e9202c509a0fc05da500a427ac06 /test/regress/regress2 | |
parent | f51d3e353fe8e50e5e73c37c17229e603a56ecdd (diff) |
Incremental support for bv_to_int (#4967)
This PR adds support for incremental solving in bv_to_int.
This amounts to:
using context dependent data structures
adding a test
In addition, we check for parametrized operations in a more robust way (using kind::metakind::PARAMETERIZED) and rename some tests for convenience.
Diffstat (limited to 'test/regress/regress2')
-rw-r--r-- | test/regress/regress2/bv_to_int_inc1.smt2 | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2 new file mode 100644 index 000000000..0d09a7252 --- /dev/null +++ b/test/regress/regress2/bv_to_int_inc1.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --incremental --solve-bv-as-int=sum +; EXPECT sat +; EXPECT sat +; EXPECT unsat +; EXPECT sat +(set-logic QF_BV) +(set-option :incremental true) +(declare-fun a () (_ BitVec 3)) +(declare-fun b () (_ BitVec 3)) +(declare-fun c () (_ BitVec 3)) + +(assert (bvult a (bvand b c))) +(check-sat) +; EXPECT: sat + +(push 1) +(assert (bvult c b)) +(check-sat) +; EXPECT: sat + + +(push 1) +(assert (bvugt c b)) +(check-sat) +; EXPECT: unsat +(pop 2) + +(check-sat) +; EXPECT: sat +(exit) |