diff options
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index a635568fe..cb8e6f200 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -924,7 +924,9 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { if( d_last_inst_si ){ Assert( d_conj->getCegConjectureSingleInv() != NULL ); sol = d_conj->getSingleInvocationSolution( i, tn, status ); - sol = sol.getKind()==LAMBDA ? sol[1] : sol; + if( !sol.isNull() ){ + sol = sol.getKind()==LAMBDA ? sol[1] : sol; + } }else{ Node cprog = d_conj->getCandidate( i ); if( !d_conj->d_cinfo[cprog].d_inst.empty() ){ |