From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 17 Nov 2014 14:33:55 +0000 (-0500)
Subject: Short-circuit in TheoryArithPrivate::check(), care of Tim.
X-Git-Tag: cvc5-1.0.0~6490
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e5e33a2de5419da0d9e43746871224eeb48bd5ed;p=cvc5.git

Short-circuit in TheoryArithPrivate::check(), care of Tim.
---

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index d6537c562..c8e7991a5 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3346,6 +3346,11 @@ bool TheoryArithPrivate::hasFreshArithLiteral(Node n) const{
 
 void TheoryArithPrivate::check(Theory::Effort effortLevel){
   Assert(d_currentPropagationList.empty());
+
+  if(done() && !Theory::fullEffort(effortLevel) && ( d_qflraStatus == Result::SAT) ){
+    return;
+  }
+
   TimerStat::CodeTimer checkTimer(d_containing.d_checkTime);
   //cout << "TheoryArithPrivate::check " << effortLevel << std::endl;
   Debug("effortlevel") << "TheoryArithPrivate::check " << effortLevel << std::endl;