From 54853f9584f2de2bf4e1ff16517b44a45e6d7cf2 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 14 Sep 2021 10:39:43 -0700
Subject: 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.
---
 test/regress/regress0/bv/bvproof1.smt2 | 4 ++++
 test/regress/regress0/bv/bvproof2.smt2 | 7 +++++++
 test/regress/regress0/bv/bvproof3.smt2 | 6 ++++++
 3 files changed, 17 insertions(+)
 create mode 100644 test/regress/regress0/bv/bvproof1.smt2
 create mode 100644 test/regress/regress0/bv/bvproof2.smt2
 create mode 100644 test/regress/regress0/bv/bvproof3.smt2

(limited to 'test/regress/regress0/bv')

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)
-- 
cgit v1.2.3