Add simple inferences for extended bitvector functions, add a few related options. Use bv2nat, int2bv as triggers. Add regressions.

1 files changed, 4 insertions, 4 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index cf7611dab..c21aa5445 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -582,6 +582,10 @@ void TheoryEngine::check(Theory::Effort effort) {
 
     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
     if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
+      Trace("theory::assertions-model") << endl;
+      if (Trace.isOn("theory::assertions-model")) {
+        printAssertions("theory::assertions-model");
+      }
       //checks for theories requiring the model go at last call
       bool builtModel = false;
       for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
@@ -607,10 +611,6 @@ void TheoryEngine::check(Theory::Effort effort) {
           // must build model at this point
           d_curr_model_builder->buildModel(d_curr_model, true);
         }
-        Trace("theory::assertions-model") << endl;
-        if (Trace.isOn("theory::assertions-model")) {
-          printAssertions("theory::assertions-model");
-        }
       }
     }