diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/issue4820.smt2 | 15 |
2 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a0fee2185..f9840e552 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -983,6 +983,7 @@ set(regress_0_tests regress0/strings/issue4376.smt2 regress0/strings/issue4662-consume-nterm.smt2 regress0/strings/issue4674-recomp-nf.smt2 + regress0/strings/issue4820.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue4820.smt2 b/test/regress/regress0/strings/issue4820.smt2 new file mode 100644 index 000000000..0bf0fac65 --- /dev/null +++ b/test/regress/regress0/strings/issue4820.smt2 @@ -0,0 +1,15 @@ +; EXPECT: sat +(set-logic QF_S) +(declare-fun _substvar_270_ () String) +(declare-fun _substvar_273_ () Bool) +(declare-fun _substvar_275_ () Bool) +(declare-fun _substvar_293_ () Bool) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const Str3 String) +(declare-const Str7 String) +(declare-const Str15 String) +(assert (or (xor true true (xor v0 v3 false v1 false v2 v2 v1 false v2 v1) true true (=> (or v1 (distinct Str15 _substvar_270_ Str3 (str.++ Str7 Str7)) v2) false) false true) _substvar_275_)) +(check-sat) |