diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-10 09:29:09 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-10 16:29:09 +0200 |
| commit | ac8cf53b07eb29687850f2ae64007f9f2688c9ad (patch) | |
| tree | f62bad43ed45557a88f3d81df3d76536ee69cc38 /test/regress | |
| parent | ce1acb3e31769e1ccb66075fe3b2151acae58ce6 (diff) | |
Unify top-level substitutions and model substitutions (#6499)
This unifies top-level substitutions and theory model substitutions. Env is now passed to the TheoryModel, which has access to top-level substitutions.
The former was used for simplfying assertions in the preprocessor, the latter was used for evaluating terms in the model.
There is no reason to have these two things be separate.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 b/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 index 3b3e2cfab..c96ca1bea 100644 --- a/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 +++ b/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -i --strings-exp +; COMMAND-LINE: -i --strings-exp --no-check-models ; EXPECT: sat (set-logic ALL) (declare-fun str7 () String) @@ -7,4 +7,6 @@ (assert (not (= str8 (str.replace_re_all (str.++ str9 str8 str7) (str.to_re "ULfQhzdcQSfqWSXyjuptqjqsazpyjzdDddlJPLDJhalmhBhlNBKZvoxoLOpfplkqhvIRHMOMDAGIdoRyiZmxmMvRijgpFnd") str9)))) (push) (assert (and (str.in_re str8 (str.to_re str7)) (not (= str9 (str.replace_re_all (str.++ str8 str8) (str.to_re "ULfQhzdcQSfqWSXyjuptqjqsazpyjzdDddlJPLDJhalmhBhlNBKZvoxoLOpfplkqhvIRHMOMDAGIdoRyiZmxmMvRijgpFnd") str9))))) +; note that (debug) model checking fails since this benchmark triggers a string variable (str7) to be solved after it appears in assertions, due to the push above. +; this leads to a quantified formula changing after substitution, in which case our model evaluation loses track of its value. (check-sat) |