diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-10-13 23:28:36 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-13 23:28:36 -0700 |
| commit | 1cecdb3b4d8be47d446be5d33cc4d3063061d2b3 (patch) | |
| tree | 11416528c4ba2132b756d4a7b39ce99387a37a79 /test/regress/regress0/bv | |
| parent | 0ddae476216452696dbb809173afc2fb440a7c57 (diff) | |
bv2int: rewritings and unsat cores (#5263)
This commit fixes several issues with bv-to-int preprocessing pass, mostly raised by @ajreynol:
1. make sure to rewrite the processed node before and after processing it
2. use the new `mkAnd` function
3. remove `--no-check-unsat-cores` from tests whenever possible
4. add new tests from #5230 . These tests now pass, and so this PR closes #5230 if merged. This also makes #5253 redundant.
5. remove an unused test
Diffstat (limited to 'test/regress/regress0/bv')
5 files changed, 33 insertions, 5 deletions
diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2 index 9111ac25c..8410d04b9 100644 --- a/test/regress/regress0/bv/bv_to_int1.smt2 +++ b/test/regress/regress0/bv/bv_to_int1.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 ; EXPECT: unsat (set-logic QF_BV) (declare-fun x () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 b/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 new file mode 100644 index 000000000..32680d862 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 @@ -0,0 +1,9 @@ +; REQUIRES: proof +; EXPECT: sat +(set-logic QF_UFBV) +(set-option :produce-unsat-cores true) +(set-option :solve-bv-as-int sum) +(declare-const v8 Bool) +(declare-const bv_14-0 (_ BitVec 14)) +(declare-const v12 Bool) +(check-sat-assuming ((! (or (= ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))) ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7)))) (= bv_14-0 bv_14-0 bv_14-0) (= ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))) ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7)))) v12) :named IP_71) (! (or v12 v8 v8 (= ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))) ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))))) :named IP_75))) diff --git a/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 b/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 new file mode 100644 index 000000000..757b00e5f --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 @@ -0,0 +1,7 @@ +; REQUIRES: proof +; EXPECT: sat +(set-logic ABV) +(set-option :check-unsat-cores true) +(set-option :solve-bv-as-int sum) +(assert (! (exists ((q4 (_ BitVec 6))) true) :named IP_2)) +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 b/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 new file mode 100644 index 000000000..e94e0cae5 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 @@ -0,0 +1,12 @@ +; REQUIRES: proof +; EXPECT: sat +(set-logic QF_UFBV) +(set-option :check-unsat-cores true) +(set-option :solve-bv-as-int sum) +(declare-const v0 Bool) +(declare-const v5 Bool) +(declare-const v8 Bool) +(declare-const v9 Bool) +(assert (or (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110) v9 (= #b1001110 ((_ sign_extend 0) #b1001110) #b1001110 #b1001110 ((_ sign_extend 0) #b1001110)) v5 (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110))) +(assert (or v0 v8)) +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2 index 42e06a940..8bf4a825d 100644 --- a/test/regress/regress0/bv/bv_to_int_zext.smt2 +++ b/test/regress/regress0/bv/bv_to_int_zext.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 ; EXPECT: unsat (set-logic QF_BV) (declare-fun T1_31078 () (_ BitVec 8)) |