diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-16 22:16:49 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-16 22:16:55 +0200 |
| commit | 9d7378688486cb0dbad207482932dfb4b5d91f95 (patch) | |
| tree | 11762aa3a877de82f3b578699c40ba37016efb79 /src/theory/quantifiers/ce_guided_instantiation.cpp | |
| parent | 6d279143db69b153815165c752eae1432538ec2e (diff) | |
Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor changes to options.
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index dddbee73b..69e8cc4e0 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -44,7 +44,8 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ if( d_guard.isNull() ){ d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); //specify guard behavior - qe->getValuation().ensureLiteral( d_guard ); + d_guard = qe->getValuation().ensureLiteral( d_guard ); + AlwaysAssert( !d_guard.isNull() ); qe->getOutputChannel().requirePhase( d_guard, true ); } } @@ -338,7 +339,7 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le Node lem = lhs.eqNode( rhs ); Node cond = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[index].getTester() ), n ); lem = NodeManager::currentNM()->mkNode( OR, cond.negate(), lem ); - + d_size_term_lemma[n][index] = lem; Trace("cegqi-lemma-debug") << "...constructed lemma " << lem << std::endl; lems.push_back( lem ); |