From: Tim King <taking@cs.nyu.edu>
Date: Mon, 14 Jun 2010 18:35:17 +0000 (+0000)
Subject: Fix to arith to make sure it only attempts to report 1 conflict per check() call.
X-Git-Tag: cvc5-1.0.0~8991
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4de93c75eb2e4d724c5c19749c81df92bde55154;p=cvc5.git

Fix to arith to make sure it only attempts to report 1 conflict per check() call.
---

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6c6a61adf..5d5313b76 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -622,7 +622,7 @@ void TheoryArith::check(Effort level){
 
   bool conflictDuringAnAssert = false;
 
-  while(!done()){
+  while(!done() && !conflictDuringAnAssert){
     //checkTableau();
     Node original = get();
     Node assertion = simulatePreprocessing(original);
@@ -633,14 +633,16 @@ void TheoryArith::check(Effort level){
 
     switch(assertion.getKind()){
     case LEQ:
-      conflictDuringAnAssert |= AssertUpper(assertion, original);
+      conflictDuringAnAssert = AssertUpper(assertion, original);
       break;
     case GEQ:
-      conflictDuringAnAssert |= AssertLower(assertion, original);
+      conflictDuringAnAssert = AssertLower(assertion, original);
       break;
     case EQUAL:
-      conflictDuringAnAssert |= AssertUpper(assertion, original);
-      conflictDuringAnAssert |= AssertLower(assertion, original);
+      conflictDuringAnAssert = AssertUpper(assertion, original);
+      if(!conflictDuringAnAssert){
+        conflictDuringAnAssert = AssertLower(assertion, original);
+      }
       break;
     case NOT:
       {
@@ -649,13 +651,13 @@ void TheoryArith::check(Effort level){
         case LEQ: //(not (LEQ x c)) <=> (GT x c)
           {
             Node pushedin = pushInNegation(assertion);
-            conflictDuringAnAssert |= AssertLower(pushedin,original);
+            conflictDuringAnAssert = AssertLower(pushedin,original);
             break;
           }
         case GEQ: //(not (GEQ x c) <=> (LT x c)
           {
             Node pushedin = pushInNegation(assertion);
-            conflictDuringAnAssert |= AssertUpper(pushedin,original);
+            conflictDuringAnAssert = AssertUpper(pushedin,original);
             break;
           }
         case EQUAL:
@@ -671,10 +673,14 @@ void TheoryArith::check(Effort level){
     }
   }
   if(conflictDuringAnAssert){
+    while(!done()) { get(); }
+
     if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
     d_partialModel.revertAssignmentChanges();
     if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
 
+
+
     //return
     return;
   }