diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-12 08:30:42 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-12 13:30:42 +0000 |
| commit | 111f98a41b488b8124fbecd28dba17465ea30786 (patch) | |
| tree | aaec0192960bdb3e47efc39917c4e2db23ea1f5d /test/regress | |
| parent | f41d71cbf1946a5ee5a63c062a23c7426ec5e87d (diff) | |
Ensure sequences of Booleans generate Boolean term variable skolems when applicable (#6529)
Fixes #6510.
This PR also eliminates a deprecated variant mkBooleanTermVariable from SkolemManager.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/issue6510-seq-bool.smt2 | 6 |
2 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 538868c6c..8ed170da9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1127,6 +1127,7 @@ set(regress_0_tests regress0/strings/issue5816-re-kind.smt2 regress0/strings/issue5915-repl-ctn-rewrite.smt2 regress0/strings/issue6203-3-unfold-trivial-true.smt2 + regress0/strings/issue6510-seq-bool.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue6510-seq-bool.smt2 b/test/regress/regress0/strings/issue6510-seq-bool.smt2 new file mode 100644 index 000000000..80bcea8a1 --- /dev/null +++ b/test/regress/regress0/strings/issue6510-seq-bool.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp -q +; EXPECT: sat +(set-logic ALL) +(declare-fun e () (Seq Bool)) +(assert (seq.nth (ite (= 0 (seq.len e)) (as seq.empty (Seq Bool)) (seq.unit false)) 0)) +(check-sat) |