diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-30 15:44:32 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-30 20:44:32 +0000 |
| commit | 007e93702d91c02954180cd601741aa19bf2a127 (patch) | |
| tree | 2d2a02f3a5ab70e590f36256b67f492e50e62596 /test | |
| parent | be403c18c6291e1cf15cdbe46489e65d9323e1b6 (diff) | |
Fix proof equality engine for "no-explain" premises (#7079)
There was an inconsistency between when the equality engine would explain a literal and when we would provide a proof for it. This led to rare cases where we over zealously provided a proof for a fact that should have been an assumption in the theory lemma proof.
This corrects the issue by ensuring that no-explain premises are explicitly marked via a new helper proof generator "AssumptionProofGenerator" which always supplies (ASSUME f) as the proof for f.
This corrects some proof checking errors on string benchmarks.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress1/strings/instance3303-delta.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress1/strings/instance7075-delta.smt2 | 6 |
3 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index dca8860fd..0d8ec19dc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2131,6 +2131,8 @@ set(regress_1_tests regress1/strings/idof-neg-index.smt2 regress1/strings/idof-triv.smt2 regress1/strings/ilc-l-nt.smt2 + regress1/strings/instance3303-delta.smt2 + regress1/strings/instance7075-delta.smt2 regress1/strings/issue1105.smt2 regress1/strings/issue1684-regex.smt2 regress1/strings/issue2060.smt2 diff --git a/test/regress/regress1/strings/instance3303-delta.smt2 b/test/regress/regress1/strings/instance3303-delta.smt2 new file mode 100644 index 000000000..b42974774 --- /dev/null +++ b/test/regress/regress1/strings/instance3303-delta.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_S) +(set-info :status unsat) +(declare-const X String) +(assert (str.in_re X (re.++ (re.range "1" "9") ((_ re.loop 0 2) (re.range "0" "9")) (str.to_re "}")))) +(assert (not (str.in_re X (re.++ (re.union (re.range "0" "9") (re.++ (re.range "1" "9") (re.range "0" "9")) (re.++ (re.range "1" "9") (re.range "0" "9") (re.range "0" "9"))) (str.to_re "}"))))) +(check-sat) diff --git a/test/regress/regress1/strings/instance7075-delta.smt2 b/test/regress/regress1/strings/instance7075-delta.smt2 new file mode 100644 index 000000000..54cd2cd9c --- /dev/null +++ b/test/regress/regress1/strings/instance7075-delta.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_S) +(set-info :status sat) +(declare-const X String) +(assert (not (str.in_re X (re.++ (re.range "0" "9") ((_ re.loop 1 2) (re.range "0" "9")))))) +(assert (str.in_re X (re.union (re.++ (re.range "0" "9") ((_ re.loop 1 6) (re.range "0" "9"))) (str.to_re "")))) +(check-sat) |