diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-09-14 10:39:43 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-14 12:39:43 -0500 |
commit | 54853f9584f2de2bf4e1ff16517b44a45e6d7cf2 (patch) | |
tree | f017fb00681a47ab412425bac93434a4e171ec16 /test | |
parent | efdefd95abd7de85963b9dd22e98e2858864cb07 (diff) |
proofs: Properly track pre- and post-rewrites in bbAtom(). (#7147)
This commit refactors the proof bit-blaster to properly track the pre- and post-rewrites in bbAtom(). The individual bit-blast steps are recorded in a term conversion proof generator. The overall bit-blast proof is stored in a BitblastProofGenerator, which tracks the pre- and post-rewrite and includes the bit-blast proof of the TCPG.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
-rw-r--r-- | test/regress/regress0/bv/bvproof1.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress0/bv/bvproof2.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/bv/bvproof3.smt2 | 6 |
4 files changed, 20 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index be95286cc..fd734b321 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -260,6 +260,9 @@ set(regress_0_tests regress0/bv/bv_to_int_zext.smt2 regress0/bv/bvcomp.cvc regress0/bv/bvmul-pow2-only.smt2 + regress0/bv/bvproof1.smt2 + regress0/bv/bvproof2.smt2 + regress0/bv/bvproof3.smt2 regress0/bv/bvsimple.cvc regress0/bv/bvsmod.smt2 regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smtv1.smt2 diff --git a/test/regress/regress0/bv/bvproof1.smt2 b/test/regress/regress0/bv/bvproof1.smt2 new file mode 100644 index 000000000..a947aa84a --- /dev/null +++ b/test/regress/regress0/bv/bvproof1.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_BV) +(set-info :status unsat) +(declare-const x Bool) +(check-sat-assuming ((not (bvuge (bvcomp (_ bv0 4) (_ bv0 4)) (ite x (_ bv1 1) (_ bv0 1)))))) diff --git a/test/regress/regress0/bv/bvproof2.smt2 b/test/regress/regress0/bv/bvproof2.smt2 new file mode 100644 index 000000000..f06194952 --- /dev/null +++ b/test/regress/regress0/bv/bvproof2.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_ABV) +(set-info :status unsat) +(declare-const v (_ BitVec 1)) +(declare-const _v (_ BitVec 2)) +(declare-fun a () (Array (_ BitVec 3) (_ BitVec 2))) +(assert (not (= (store (store (store a ((_ zero_extend 1) _v) (_ bv0 2)) (_ bv1 3) (_ bv0 2)) (_ bv0 3) (_ bv0 2)) (store (store (store (store a (_ bv0 3) (_ bv0 2)) ((_ zero_extend 2) v) (_ bv0 2)) (_ bv1 3) (_ bv0 2)) ((_ zero_extend 1) _v) (_ bv0 2))))) +(check-sat) diff --git a/test/regress/regress0/bv/bvproof3.smt2 b/test/regress/regress0/bv/bvproof3.smt2 new file mode 100644 index 000000000..5650bc5d6 --- /dev/null +++ b/test/regress/regress0/bv/bvproof3.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --bitblast=eager +(set-logic QF_BV) +(set-info :status unsat) +(declare-const x (_ BitVec 1)) +(assert (= (_ bv2 4) ((_ zero_extend 3) x))) +(check-sat) |