From b3f05d5c25facaf0c34ee79faed060bda3f61a8d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 11 Feb 2021 08:08:57 -0600 Subject: [PATCH] Fix spurious assertion failure in regexp normalization (#5852) Fixes #5816. --- src/theory/strings/regexp_solver.cpp | 3 ++- test/regress/CMakeLists.txt | 1 + test/regress/regress0/strings/issue5816-re-kind.smt2 | 6 ++++++ 3 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/strings/issue5816-re-kind.smt2 diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 3f419c66d..46570df48 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -664,7 +664,8 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector& nf_exp) switch (r.getKind()) { case REGEXP_EMPTY: - case REGEXP_SIGMA: break; + case REGEXP_SIGMA: + case REGEXP_RANGE: break; case STRING_TO_REGEXP: { if (!r[0].isConst()) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index edf49b502..d455bb85b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1114,6 +1114,7 @@ set(regress_0_tests regress0/strings/issue5745-eager-pp.smt2 regress0/strings/issue5767-eager-pp.smt2 regress0/strings/issue5771-eager-pp.smt2 + regress0/strings/issue5816-re-kind.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue5816-re-kind.smt2 b/test/regress/regress0/strings/issue5816-re-kind.smt2 new file mode 100644 index 000000000..a1e7eb7f4 --- /dev/null +++ b/test/regress/regress0/strings/issue5816-re-kind.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status sat) +(declare-const x String) +(declare-const x8 String) +(assert (str.in_re x8 (re.++ (str.to_re x) (re.range "a" "u")))) +(check-sat) -- 2.30.2