From 5634dc5875f77dedfbb5599bdc56176582c6da8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Jan 2025 17:50:15 -0800 Subject: [PATCH] fix model construction bug: ignore non-relevant expressions when building model Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_context.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index 09657500d..86c4900df 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -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);