From fb746fdd4e60e7d166b0fa1e5788bea925d22ee7 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 21 Aug 2015 10:07:12 +0200
Subject: Fix disequality bounds in cbqi, record literals for ITE skolems in
 cbqi.  Enable redundant ITE branch elimination in quantifiers rewriter.

---
 src/theory/quantifiers_engine.cpp | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/theory/quantifiers_engine.cpp')

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 13c408d85..d1a268950 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -329,6 +329,10 @@ void QuantifiersEngine::check( Theory::Effort e ){
       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
       debugPrintEqualityEngine( "quant-engine-ee" );
     }
+    if( Trace.isOn("quant-engine-assert") ){
+      Trace("quant-engine-assert") << "Assertions : " << std::endl;
+      getTheoryEngine()->printAssertions("quant-engine-assert");
+    }
 
     //reset relevant information
     d_conflict = false;
-- 
cgit v1.2.3