diff options
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 57c5533a9..96bb9a9f7 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -349,7 +349,7 @@ bool ConjectureGenerator::hasEnumeratedUf( Node n ) { if( !lem.empty() ){ for (const Node& l : lem) { - d_qim.addPendingLemma(l); + d_qim.addPendingLemma(l, InferenceId::UNKNOWN); } d_hasAddedLemma = true; return false; @@ -934,7 +934,7 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in d_eq_conjectures[rhs].push_back( lhs ); Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg ); - d_qim.addPendingLemma(lem); + d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); d_qim.addPendingPhaseRequirement(rsg, false); addedLemmas++; if( (int)addedLemmas>=options::conjectureGenPerRound() ){ |