diff options
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) |