diff options
Diffstat (limited to 'src/smt/unsat_core_manager.cpp')
| -rw-r--r-- | src/smt/unsat_core_manager.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index ba2c07326..22304f9e8 100644 --- a/src/smt/unsat_core_manager.cpp +++ b/src/smt/unsat_core_manager.cpp @@ -80,7 +80,10 @@ void UnsatCoreManager::getRelevantInstantiations( const std::vector<Node>& instTerms = cur->getArguments(); Assert(cs.size() == 1); Node q = cs[0]->getResult(); - insts[q].push_back({instTerms.begin(), instTerms.end()}); + // the instantiation is a prefix of the arguments up to the number of + // variables + insts[q].push_back( + {instTerms.begin(), instTerms.begin() + q[0].getNumChildren()}); } for (const std::shared_ptr<ProofNode>& cp : cs) { |