mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-22 06:55:51 +00:00
Code Activity

disable instantiation for inconsistent states

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-15 20:54:23 -07:00
parent 9945e3dc9a
commit 09ffec52e8
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/qi_queue.cpp
View file

@ -197,6 +197,9 @@ namespace smt {
}
void qi_queue::instantiate(entry & ent) {
if (m_context.inconsistent())
return;
// set temporary flag to enable quantifier-specific tracing in within smt_internalizer.
flet<bool> _coming_from_quant(m_context.m_coming_from_quant, true);