Enable multi-trigger-linear by default, add option.

1 files changed, 3 insertions, 3 deletions

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index d4d6cfb00..f2a4e6d17 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -58,11 +58,11 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
       d_mg->setActiveAdd(true);
     }
   }else{
-    if( options::multiTriggerLinear() ){
+    if( options::multiTriggerCache() ){
+      d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe );
+    }else{
       d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti( f, d_nodes, qe );
       d_mg->setActiveAdd(true);
-    }else{
-      d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe );
     }
     //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe );
     //d_mg->setActiveAdd();