diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-11 08:08:57 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-11 08:08:57 -0600 |
| commit | b3f05d5c25facaf0c34ee79faed060bda3f61a8d (patch) | |
| tree | de3c78c339cc86a62b07dce37537c28339b6513a | |
| parent | b10e383e5efc92f02c63eaf5eec07479ed385304 (diff) | |
Fix spurious assertion failure in regexp normalization (#5852)
Fixes #5816.
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 3 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/issue5816-re-kind.smt2 | 6 |
3 files changed, 9 insertions, 1 deletions
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<Node>& 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) |