mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

filter instantiations for model values to fix issue #183

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-06 14:43:08 +02:00
parent f96c0b6963
commit 6780784bcf
2 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_model_checker.cpp
View file

@ -170,11 +170,9 @@ namespace smt {
if (sk_term != 0) { if (sk_term != 0) {
sk_value = sk_term; sk_value = sk_term;
} }
else {
if (m_manager.is_model_value(sk_value))
return false;
}
} }
if (m_manager.is_model_value(sk_value))
return false;
bindings.set(num_decls - i - 1, sk_value); bindings.set(num_decls - i - 1, sk_value);
} }

1
src/smt/smt_model_finder.cpp
View file

@ -102,6 +102,7 @@ namespace smt {
return; return;
m_manager.inc_ref(n); m_manager.inc_ref(n);
m_elems.insert(n, generation); m_elems.insert(n, generation);
CTRACE("model_finder", m_manager.is_model_value(n), tout << mk_pp(n, m_manager) << "\n";);
SASSERT(!m_manager.is_model_value(n)); SASSERT(!m_manager.is_model_value(n));
} }