From 0faead1572109c1d7cb3d67647da02d0b4600a20 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 23 Aug 2019 17:27:05 -0500 Subject: Infer emptiness instead of splitting when a string equality rewrites to a constant (#3218) --- test/regress/regress1/strings/issue3217.smt2 | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test/regress/regress1/strings/issue3217.smt2 (limited to 'test/regress/regress1') diff --git a/test/regress/regress1/strings/issue3217.smt2 b/test/regress/regress1/strings/issue3217.smt2 new file mode 100644 index 000000000..4fd35999d --- /dev/null +++ b/test/regress/regress1/strings/issue3217.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL_SUPPORTED) +(set-option :strings-exp true) +(set-info :status unsat) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(declare-fun d () String) +(assert + (or + (not (= ( str.suffixof "B" ( str.replace "A" b "B")) (= ( str.substr a 0 (str.len b)) "A"))) + (not (= (not (= c "A")) ( str.suffixof "A" ( str.replace "A" c "B")))))) +(assert (= a (str.++ (str.++ b "") d))) +(check-sat) -- cgit v1.2.3