diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-11 15:04:35 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-11 15:04:35 -0600 |
| commit | 49215e6948aba1d6b762e28a7293581e25c2df8c (patch) | |
| tree | c769369b913bb383c714ae68c575add32e3d06e1 /test/regress/regress1/strings | |
| parent | e4fd524b02054a3ac9724f184e55a983cb6cb6b9 (diff) | |
Fix length assumption for deq norm emp rule (#5623)
There is an assumption that is not guaranteed to hold in this rule, thus we should not try to explain in the equality engine.
Fixes #5611.
Note this inference was not previously covered in our coverage build.
Diffstat (limited to 'test/regress/regress1/strings')
| -rw-r--r-- | test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 b/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 new file mode 100644 index 000000000..3b3e2cfab --- /dev/null +++ b/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: -i --strings-exp +; EXPECT: sat +(set-logic ALL) +(declare-fun str7 () String) +(declare-fun str8 () String) +(declare-fun str9 () String) +(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))))) +(check-sat) |