diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-05 15:52:20 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-05 20:52:20 +0000 |
| commit | 3c98bb2e9abdb2542ac794f161d0f199c1cfaeaf (patch) | |
| tree | 12de562c61aae8ad066fcd33444ab4ee639d822b /src | |
| parent | e95e704f362690377d851fe80bbc778877bbfc69 (diff) | |
Fix spurious antecedant for symbolic regular expressions (#6284)
Fixes #6271.
This was triggered by recent fixes, this fixes solution soundness issues with symbolic regular expressions due to spuriously included antecedants, which made lemmas SAT-context dependent while being cached as user-context dependent.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 0db536d1b..7510b26ca 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -265,11 +265,11 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) // if so, do simple unrolling Trace("strings-regexp") << "Simplify on " << atom << std::endl; Node conc = d_regexp_opr.simplify(atom, polarity); - Trace("strings-regexp") << "...finished" << std::endl; + Trace("strings-regexp") << "...finished, got " << conc << std::endl; // if simplifying successfully generated a lemma if (!conc.isNull()) { - std::vector<Node> iexp = rnfexp; + std::vector<Node> iexp; std::vector<Node> noExplain; iexp.push_back(assertion); noExplain.push_back(assertion); |