From 4de93c75eb2e4d724c5c19749c81df92bde55154 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Mon, 14 Jun 2010 18:35:17 +0000
Subject: [PATCH] Fix to arith to make sure it only attempts to report 1
 conflict per check() call.

---
 src/theory/arith/theory_arith.cpp | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

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;
   }
-- 
2.30.2