From 089a60266f2658e471d204fdd737e3e0d37e105c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 19 Mar 2020 07:18:58 -0700 Subject: Only apply testConstStringInRegExp to const regexp (#4120) Fixes #4070. `TheoryStringsRewriter::rewriteConcatRegExp()` rewrites `(a)* ++ (_)*` to `(_)*`. To do so, it checks whether the elements preceding `(_)*` match the empty string using `TheoryStringsRewriter::testConstStringInRegExp()`. However, this method only expects to be called on constant regular expressions (i.e. regular expressions without string variables). This commit adds a corresponding check before calling `TheoryStringsRewriter::testConstStringInRegExp()`. --- test/regress/regress0/strings/issue4070.smt2 | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test/regress/regress0/strings/issue4070.smt2 (limited to 'test/regress/regress0/strings/issue4070.smt2') diff --git a/test/regress/regress0/strings/issue4070.smt2 b/test/regress/regress0/strings/issue4070.smt2 new file mode 100644 index 000000000..2de58c4d2 --- /dev/null +++ b/test/regress/regress0/strings/issue4070.smt2 @@ -0,0 +1,6 @@ +; EXPECT: sat +(set-logic QF_S) +(declare-fun a () String) +(declare-fun b () String) +(assert (str.in.re a (re.++ (str.to.re b) (re.* re.allchar)))) +(check-sat) -- cgit v1.2.3