From 5494fb086071c6e68cb5125932af0126c5b9d42e Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 25 Oct 2014 09:55:16 +0200
Subject: [PATCH] Minor fix for --user-pat=resort

---
 src/theory/quantifiers/inst_strategy_e_matching.cpp | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index e95936220..4284c8145 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -65,16 +65,19 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
       return STATUS_UNFINISHED;
     }else if( e==peffort ){
       d_counter[f]++;
-      
+
       Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl;
       if( options::userPatternsQuant()==USER_PAT_MODE_RESORT  ){
         int matchOption = 0;
         for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){
-          d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], matchOption, true, Trigger::TR_RETURN_NULL, options::smartTriggers() ) );
+          Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], matchOption, true, Trigger::TR_RETURN_NULL, options::smartTriggers() );
+          if( t ){
+            d_user_gen[f].push_back( t );
+          }
         }
         d_user_gen_wait[f].clear();
       }
-      
+
       for( unsigned i=0; i<d_user_gen[f].size(); i++ ){
         bool processTrigger = true;
         if( processTrigger ){
-- 
2.30.2