#7362

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 30, 2024 · 9a87bb1 · 9a87bb1
1 parent 46d602e
commit 9a87bb1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
@@ -457,7 +457,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 if (interp) {
                     var_subst vs(m, false);
                     result = vs(fi->get_interp(), num, args);
-                    result = m.mk_ite(m.mk_eq(m_au.mk_real(rational(0)), args[1]), result, m.mk_app(f, num, args));
+                    result = m.mk_ite(m.mk_eq(m_au.mk_numeral(rational(0), args[1]->get_sort()), args[1]), result, m.mk_app(f, num, args));
                     return BR_DONE;
                 }
             }