disable expensive model validation

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/smt/smt_conflict_resolution.cpp

@@ -506,6 +506,7 @@ namespace smt {
             case b_justification::CLAUSE: {
                 clause * cls = js.get_clause();
                 TRACE("conflict", m_ctx.display_clause_detail(tout, cls););
+                TRACE("conflict", tout << literal_vector(cls->get_num_literals(), cls->begin()) << "\n";);
                 if (cls->is_lemma())
                     cls->inc_clause_activity();
                 unsigned num_lits = cls->get_num_literals();

src/smt/smt_context.cpp

@@ -3342,6 +3342,7 @@ namespace smt {
             for (theory* t : m_theory_set) {
                 t->validate_model(*m_model);
             }
+#if 0
             for (literal lit : m_assigned_literals) {
                 if (!is_relevant(lit)) continue;
                 expr* v = m_bool_var2expr[lit.var()];
@@ -3364,6 +3365,7 @@ namespace smt {
                     IF_VERBOSE(10, display_clause_smt2(verbose_stream() << "not satisfied:\n", *cls) << "\n");                    
                 }
             }
+#endif
         }
         return r;
     }

src/smt/smt_internalizer.cpp

@@ -1340,7 +1340,6 @@ namespace smt {
             break;
         }
         TRACE("mk_clause", tout << "after simplification:\n"; display_literals_verbose(tout, num_lits, lits) << "\n";);
-        TRACE("mk_clause", tout << "after simplification:\n"; display_literals_smt2(tout, num_lits, lits););
         unsigned activity = 0;
         if (activity == 0)
             activity = 1;

src/smt/theory_seq.cpp

@@ -4186,7 +4186,6 @@ void theory_seq::validate_model(model& mdl) {
             IF_VERBOSE(0, verbose_stream() << l << " = " << r << " but " << mdl(l) << " != " << mdl(r) << "\n");
         }
     }
-
     for (auto const& ne : m_nqs) {
         expr_ref l = ne.l();
         expr_ref r = ne.r();