diff options
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/inference_manager.cpp | 1 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 6cc1e7b44..97f9666bd 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -274,6 +274,7 @@ bool InferenceManager::sendSplit(Node a, Node b, const char* c, bool preq) void InferenceManager::sendPhaseRequirement(Node lit, bool pol) { + lit = Rewriter::rewrite(lit); d_pendingReqPhase[lit] = pol; } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 2f51000ab..65f06c008 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2800,6 +2800,7 @@ void TheoryStrings::checkCodes() Node eqn = c1[0].eqNode(c2[0]); // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn); + d_im.sendPhaseRequirement(deq, false); d_im.sendInference(d_empty_vec, inj_lem, "Code_Inj"); } } |