From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 19 May 2014 02:06:29 +0000 (-0500)
Subject: minor fix for string equality engine assertion.
X-Git-Tag: cvc5-1.0.0~6900
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3ce2f2590ba541e901403707e924ad10f0b5f7d5;p=cvc5.git

minor fix for string equality engine assertion.
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0b161570a..0f9def3ea 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -732,6 +732,15 @@ void TheoryStrings::assertPendingFact(Node fact, Node exp) {
     }
     d_equalityEngine.assertEquality( atom, polarity, exp );
   } else {
+    if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
+      addMembership(fact);
+    } else if (atom.getKind() == kind::STRING_STRCTN) {
+      if(polarity) {
+        d_str_pos_ctn.push_back( atom );
+      } else {
+        d_str_neg_ctn.push_back( atom );
+      }
+    }
     d_equalityEngine.assertPredicate( atom, polarity, exp );
   }
 }
@@ -741,7 +750,7 @@ void TheoryStrings::doPendingFacts() {
   while( !d_conflict && i<d_pending.size() ) {
     Node fact = d_pending[i];
     Node exp = d_pending_exp[ fact ];
-    if(fact.getKind() == kind::STRING_CONCAT) {
+    if(fact.getKind() == kind::AND) {
       for(size_t j=0; j<fact.getNumChildren(); j++) {
         assertPendingFact(fact[j], exp);
       }
@@ -1128,7 +1137,7 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
         d_regexp_ant[str_in_re] = ant;
       }
 
-      //if(conc.isNull() || conc.getKind() == kind::OR) {
+      //if(conc.isNull() || conc == d_false || conc.getKind() == kind::OR) {
         sendLemma( ant, conc, "LOOP-BREAK" );
       //} else {
         //sendInfer( ant, conc, "LOOP-BREAK" );