diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-07 12:44:20 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-07 17:44:20 +0000 |
| commit | 7e9e71c7bd2bcbdcb2cef0d8f99bf34082bf4081 (patch) | |
| tree | 201fe80043ddb91a72f56f34c2906ef990ad6faf /test/regress | |
| parent | 4cb2b23322794fc684db4f4a9f9e14e0157c83b0 (diff) | |
(proof-new) Fix missing connection in trust substitution proofs (#6685)
This PR fixes a missing connection in trust substitution proofs, which was the cause of open proofs when solved equalities from ppAssert were not justified by proofs.
Also distinguishes TRUST_SUBS_EQ from TRUST_SUBS_MAP for clarity.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bv/core/bitvec1.smtv1.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/bv/core/bitvec3.smtv1.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/bv/core/constant_core.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/cores/issue3455.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/proofs/trust-subs-eq-open.smt2 | 8 |
6 files changed, 13 insertions, 4 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 237ca77dd..207840516 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -806,6 +806,7 @@ set(regress_0_tests regress0/printer/tuples_and_records.cvc regress0/proofs/issue277-circuit-propagator.smt2 regress0/proofs/scope.smt2 + regress0/proofs/trust-subs-eq-open.smt2 regress0/push-pop/boolean/fuzz_12.smt2 regress0/push-pop/boolean/fuzz_13.smt2 regress0/push-pop/boolean/fuzz_14.smt2 diff --git a/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 b/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 index 78dd44d66..63273b899 100644 --- a/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 +++ b/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs +; COMMAND-LINE: ; EXPECT: unsat (set-option :incremental false) (set-info :source "Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. diff --git a/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 b/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 index b149c0570..79af1ce94 100644 --- a/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 +++ b/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs +; COMMAND-LINE: ; EXPECT: unsat (set-option :incremental false) (set-info :source "Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2 index f9d2e022d..e433e58e2 100644 --- a/test/regress/regress0/bv/core/constant_core.smt2 +++ b/test/regress/regress0/bv/core/constant_core.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs +; COMMAND-LINE: ; EXPECT: unsat (set-logic QF_BV) (set-info :smt-lib-version 2.6) diff --git a/test/regress/regress0/cores/issue3455.smt2 b/test/regress/regress0/cores/issue3455.smt2 index ec72daa32..7050e8c7d 100644 --- a/test/regress/regress0/cores/issue3455.smt2 +++ b/test/regress/regress0/cores/issue3455.smt2 @@ -13,4 +13,4 @@ (assert (<= x0 (- 13))) (check-sat) (check-sat) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/proofs/trust-subs-eq-open.smt2 b/test/regress/regress0/proofs/trust-subs-eq-open.smt2 new file mode 100644 index 000000000..5f6bd9ef9 --- /dev/null +++ b/test/regress/regress0/proofs/trust-subs-eq-open.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun c () (_ BitVec 3)) +(check-sat-assuming ( +(and +(= (_ bv0 1) ((_ extract 1 1) c)) +(= (_ bv1 1) ((_ extract 0 0) c)) +(not (= (_ bv1 2) ((_ extract 1 0) c)))))) |