mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix model construction bug: ignore non-relevant expressions when building model

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-26 17:50:15 -08:00
parent d3bf25ce85
commit 5634dc5875
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/sls/sls_context.cpp
View file

@ -160,6 +160,8 @@ namespace sls {
for (expr* e : subterms()) {
if (!is_app(e))
continue;
if (!is_relevant(e))
continue;
auto f = to_app(e)->get_decl();
if (!include_func_interp(f))
continue;
@ -177,6 +179,10 @@ namespace sls {
SASSERT(f->get_arity() == args.size());
if (!fi->get_entry(args.data()))
fi->insert_new_entry(args.data(), v);
else if (fi->get_entry(args.data())->get_result() != v) {
IF_VERBOSE(0, verbose_stream() << "conflict: " << mk_pp(e, m) << " " << v << " " << mk_pp(fi->get_entry(args.data())->get_result(), m) << "\n");
throw default_exception("conflicting assignment");
}
}
s.on_model(mdl);