diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-20 17:49:27 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-20 17:49:27 -0600 |
| commit | 6edbfc98df1e9302f5051e33accc328ad7250c2b (patch) | |
| tree | 773ca11be3344097fbab85211c1fa2459b20105e /test/regress | |
| parent | 6a02b2e28ee8d0560c923eaf0073c2fdce8fbfa2 (diff) | |
Fix remove term formula policy for terms beneath quantifiers (#5497)
Now that extended arithmetic symbols are not eliminated during expandDefinitions, this allowed for a chain of events that would not apply theory preprocessing on certain terms.
In particular, a term t would not have theory preprocessing applied to it if it was a strict subterm of ITE-term s that occurred in a term position in a quantified formula body, and s did not have free variables. In this case, term formula removal would add a lemma corresponding to the ITE skolem definition, whose subterms did not have theory preprocessing applied. This meant that a (div a d) term was not being preprocessed in #5482, leading to solution unsoundness.
This changes the policy in term formula removal to be in sync with theory preprocessing: term formula removal and theory preprocessing only apply to terms that are not beneath quantifiers. In particular, this means that ground terms in quantifier bodies are left untouched until they are introduced e.g. by instantiation.
This fixes the solution soundness issue (fixes #5482).
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2 | 15 |
2 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cb37b428e..af238db18 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1616,6 +1616,7 @@ set(regress_1_tests regress1/quantifiers/issue5469-aext.smt2 regress1/quantifiers/issue5470-aext.smt2 regress1/quantifiers/issue5471-aext.smt2 + regress1/quantifiers/issue5482-rtf-no-fv.smt2 regress1/quantifiers/issue5484-qe.smt2 regress1/quantifiers/issue5484b-qe.smt2 regress1/quantifiers/issue993.smt2 diff --git a/test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2 b/test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2 new file mode 100644 index 000000000..b1e6911cd --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: unsat +(set-logic AUFNIA) +(declare-fun a () Int) +(declare-fun b () (Array Int Int)) +(declare-fun c () (Array Int Int)) +(declare-fun d () Int) +(assert + (exists ((e Int)) + (and (<= e 0) + (exists ((f Int)) + (and (<= 0 f e) + (> (select (store b 0 (select c (div a d))) f) + (select (store b 0 (select c (div a d))) e))))))) +(check-sat) |