Add sets regression, fixes bug 754. Minor fix to regexp in strings.

2 files changed, 8 insertions, 5 deletions

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 1112c2ef2..e9ac9b484 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -605,7 +605,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
     Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
     sr = d_quantEngine->getModel()->getCurrentModelValue( sr );
     Trace("bound-int-rsi") << "Value is " << sr << std::endl;
-    //map to term model
+    //as heuristic, map to term model
     if( sr.getKind()!=EMPTYSET ){
       std::map< Node, Node > val_to_term;
       while( sr.getKind()==UNION ){
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index db07a0b51..6c4a00541 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4273,10 +4273,13 @@ void TheoryStrings::checkMemberships() {
   for( unsigned i=0; i<mems.size(); i++ ){
     Node n = mems[i];
     Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
-    Assert( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 );
-    bool pol = d_extf_info_tmp[n].d_pol==1;
-    Trace("strings-process-debug") << "  add membership : " << n << ", pol = " << pol << std::endl;
-    addMembership( pol ? n : n.negate() );
+    if( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 ){
+      bool pol = d_extf_info_tmp[n].d_pol==1;
+      Trace("strings-process-debug") << "  add membership : " << n << ", pol = " << pol << std::endl;
+      addMembership( pol ? n : n.negate() );
+    }else{
+      Trace("strings-process-debug") << "  irrelevant (non-asserted) membership : " << n << std::endl;
+    }
   }
 
   bool addedLemma = false;