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/regress2 | |
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/regress2')
-rw-r--r-- | test/regress/regress2/bv_to_int_ashr.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress2/bv_to_int_mask_array_3.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress2/bv_to_int_shifts.smt2 | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2 index 5516f974b..b95dc6b7f 100644 --- a/test/regress/regress2/bv_to_int_ashr.smt2 +++ b/test/regress/regress2/bv_to_int_ashr.smt2 @@ -1,5 +1,5 @@ -; 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=8 --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=8 ; EXPECT: unsat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2 index 37582d9d8..74e5ca95a 100644 --- a/test/regress/regress2/bv_to_int_mask_array_3.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_3.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: sat (set-logic ALL) (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4))) diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2 index 7971b2bfe..bcc31c38c 100644 --- a/test/regress/regress2/bv_to_int_shifts.smt2 +++ b/test/regress/regress2/bv_to_int_shifts.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: sat (set-logic QF_BV) (declare-fun s () (_ BitVec 4)) |