From 314db5e1c4fdbfca001b1f3a679831d086b25e5c Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 7 Dec 2016 15:26:12 -0600
Subject: [PATCH] Add sets regression, fixes bug 754.  Minor fix to regexp in
 strings.

---
 src/theory/quantifiers/bounded_integers.cpp |  2 +-
 src/theory/strings/theory_strings.cpp       | 11 +++++++----
 test/regress/regress0/sets/Makefile.am      |  3 ++-
 test/regress/regress0/sets/card.smt2        |  1 +
 4 files changed, 11 insertions(+), 6 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;
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index ab597350e..d509a9fd5 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -64,7 +64,8 @@ TESTS =	\
 	union-2.smt2 \
 	dt-simp-mem.smt2 \
 	card3-ground.smt2 \
-	card-3sets.cvc
+	card-3sets.cvc \
+	card.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/card.smt2 b/test/regress/regress0/sets/card.smt2
index 6b8c536d5..d42bf6f55 100644
--- a/test/regress/regress0/sets/card.smt2
+++ b/test/regress/regress0/sets/card.smt2
@@ -1,4 +1,5 @@
 (set-logic QF_UFLIAFS)
+(set-info :status unsat)
 (declare-sort E 0)
 (declare-fun s () (Set E))
 (declare-fun t () (Set E))
-- 
2.30.2