diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-22 09:51:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-22 09:51:05 -0500 |
| commit | 93fd4aed186c3dfa1b0fa7bec102f5b94edca322 (patch) | |
| tree | 331b0bd9dcc69c2355887db5ca5fd1a20d6a63e3 /test/regress/regress1 | |
| parent | c0d4ac3d307b13c24471da5af2f916569a7f52b9 (diff) | |
Guard for non-unique skolems in term formula removal (#6179)
In rare cases, we may reuse skolems for different terms (those that are the same up to purification) due to recent changes in how skolem are generated. This guards for this case in the term formula remover, which avoids assertion failures in cd insert hash map.
Fixes #6132.
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/strings/issue6132-non-unique-skolem.smt2 | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/issue6132-non-unique-skolem.smt2 b/test/regress/regress1/strings/issue6132-non-unique-skolem.smt2 new file mode 100644 index 000000000..29d0e9469 --- /dev/null +++ b/test/regress/regress1/strings/issue6132-non-unique-skolem.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(declare-fun str () String) +(assert (= 0 (ite (= str (str.from_code + (ite (= 0 (ite (> (str.len (str.from_int (str.len str))) 1) 1 0)) 1 0))) 1 0))) +(check-sat) |