Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.

1 files changed, 1 insertions, 2 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4104c0916..948e42857 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2641,8 +2641,7 @@ void SmtEnginePrivate::processAssertions() {
 
   if( options::sortInference() ){
     //sort inference technique
-    SortInference si;
-    si.simplify( d_assertionsToPreprocess );
+    d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess );
   }
 
   dumpAssertions("pre-simplify", d_assertionsToPreprocess);