From: Tim King <taking@cs.nyu.edu>
Date: Tue, 7 May 2013 04:44:27 +0000 (-0400)
Subject: Disabling an incorrect prototyping line from the simplex merges.  Fixes bug 510.
X-Git-Tag: cvc5-1.0.0~7287^2~148
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e7519f8b5020259bd02f01c24bed74cf0e0c8be2;p=cvc5.git

Disabling an incorrect prototyping line from the simplex merges.  Fixes bug 510.
---

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index a49d3776d..9c43ca962 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1867,7 +1867,6 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
   if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel)){
     emmittedConflictOrSplit = splitDisequalities();
   }
-  emmittedConflictOrSplit = false;
 
   if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel) && !hasIntegerModel()){
     Node possibleConflict = Node::null();