From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 19 Nov 2013 23:09:19 +0000 (-0600)
Subject: Bug fix for previous commit
X-Git-Tag: cvc5-1.0.0~7248
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f806a8eedf01753116c225b4c1a5e29543fda370;p=cvc5.git

Bug fix for previous commit
---

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 5f63fa8df..dab105d20 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1648,16 +1648,18 @@ void StrongSolverTheoryUF::propagate( Theory::Effort level ){
 /** get next decision request */
 Node StrongSolverTheoryUF::getNextDecisionRequest(){
   //request the combined cardinality as a decision literal, if not already asserted
-  int comCard = 0;
-  Node com_lit;
-  do {
-    com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null();
-    if( d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){
-      Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl;
-      return com_lit;
-    }
-    comCard++;
-  }while( !com_lit.isNull() );
+  if( options::ufssFairness() ){
+    int comCard = 0;
+    Node com_lit;
+    do {
+      com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null();
+      if( !com_lit.isNull() && d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){
+        Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl;
+        return com_lit;
+      }
+      comCard++;
+    }while( !com_lit.isNull() );
+  }
   //otherwise, check each individual sort
   for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
     Node n = it->second->getNextDecisionRequest();