From 8dc1280a5161633fddfb8334811a86c911bb25c1 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 2 Sep 2014 18:28:52 -0400
Subject: check() optimization

Details of testing here:
http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
---
 src/theory/uf/theory_uf.cpp | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/theory/uf/theory_uf.cpp')

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 0da8e8c32..4fcf4166b 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -89,6 +89,10 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) {
 }/* mkAnd() */
 
 void TheoryUF::check(Effort level) {
+  if (done() && !fullEffort(level)) {
+    return;
+  }
+
   while (!done() && !d_conflict)
   {
     // Get all the assertions
-- 
cgit v1.2.3