diff options
| author | Clark Barrett <barrett@cs.stanford.edu> | 2016-12-02 14:17:49 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-12-02 14:17:49 -0800 |
| commit | 8f8e1b01ba012c438ce76701f185006364a5c448 (patch) | |
| tree | a2413139c083e54c0fc7cc4c118ec8eae20490e2 /test | |
| parent | c3c8d013d2a879eaa1d205e57af32a7f8bb8c0b7 (diff) | |
| parent | 05c7d36e7a4844ac1c8a14035776fbba6e00704b (diff) | |
Merge pull request #113 from 4tXJ7f/remove_extract_rule
Remove wrong `ExtractMultLeadingBit` rule
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/bv/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 | 7 |
2 files changed, 9 insertions, 1 deletions
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index b3c7250ff..2caaea799 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -112,7 +112,8 @@ CVC_TESTS = bvsimple.cvc sizecheck.cvc BUG_TESTS = \ bug260a.smt \ bug260b.smt \ - bug440.smt + bug440.smt \ + bug_extract_mult_leading_bit.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 b/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 new file mode 100644 index 000000000..8e3728587 --- /dev/null +++ b/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_BV) +(set-info :status sat) +(declare-fun x1 () (_ BitVec 15)) +(declare-fun x2 () (_ BitVec 15)) +(assert (not (= ((_ extract 64 60) (bvmul (concat #b00000000000000000000000000000000000000000000000000 x1) (concat #b10000000000000000000000000000000000000000000000000 x2))) #b00000))) +(check-sat) +(exit) |