diff options
Diffstat (limited to 'test/regress/regress0/strings')
4 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/issue5608-eager-pp.smt2 b/test/regress/regress0/strings/issue5608-eager-pp.smt2 new file mode 100644 index 000000000..a1a166277 --- /dev/null +++ b/test/regress/regress0/strings/issue5608-eager-pp.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --no-strings-lazy-pp -i +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +(set-logic QF_SLIA) +(declare-fun v6 () Bool) +(declare-fun str6 () String) +(assert (and v6 (str.in_re (str.replace str6 (str.from_int 12) str6) (str.to_re str6)))) +(check-sat) +(check-sat) +(assert (not v6)) +(check-sat) diff --git a/test/regress/regress0/strings/issue5745-eager-pp.smt2 b/test/regress/regress0/strings/issue5745-eager-pp.smt2 new file mode 100644 index 000000000..b869a9ded --- /dev/null +++ b/test/regress/regress0/strings/issue5745-eager-pp.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --no-strings-lazy-pp +; EXPECT: sat +(set-logic ALL) +(declare-fun i0 () Int) +(declare-fun str4 () String) +(assert (= str4 (str.substr str4 (mod i0 2) 1))) +(assert (not (= "" str4))) +(check-sat) diff --git a/test/regress/regress0/strings/issue5767-eager-pp.smt2 b/test/regress/regress0/strings/issue5767-eager-pp.smt2 new file mode 100644 index 000000000..5e4d29d5a --- /dev/null +++ b/test/regress/regress0/strings/issue5767-eager-pp.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-strings-lazy-pp -q +; EXPECT: sat +(set-logic ALL) +(declare-fun s () String) +(assert (xor (= (str.at s (div 0 0)) "A") (= (div 0 (str.len s)) 0))) +(check-sat) diff --git a/test/regress/regress0/strings/issue5771-eager-pp.smt2 b/test/regress/regress0/strings/issue5771-eager-pp.smt2 new file mode 100644 index 000000000..c3049e72f --- /dev/null +++ b/test/regress/regress0/strings/issue5771-eager-pp.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-strings-lazy-pp +; EXPECT: sat +(set-logic ALL) +(declare-fun a () Int) +(assert (str.suffixof "B" (str.from_code a))) +(check-sat) |