From 85b672ee85bf79b4f215366f2f5b74690c0a6a8e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 4 Jun 2021 17:54:19 -0700 Subject: [PATCH] #5324 --- src/sat/smt/q_mbi.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 582911222..39218d612 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -114,6 +114,8 @@ namespace q { args.push_back(replace_model_value(arg)); return expr_ref(m.mk_app(to_app(e)->get_decl(), args), m); } + if (m.is_model_value(e)) + return expr_ref(m.mk_model_value(0, e->get_sort()), m); return expr_ref(e, m); }