fix processing of else expression for model table

Z3Prover · May 2, 2023 · 392266c · 392266c
1 parent d5231f8
commit 392266c
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
@@ -146,7 +146,8 @@ void func_interp::set_else(expr * e) {
 
     ptr_vector<expr> args;
     while (e && is_fi_entry_expr(e, args)) {
-        insert_entry(args.data(), to_app(e)->get_arg(1));
+        if (!get_entry(args.data()))
+            insert_entry(args.data(), to_app(e)->get_arg(1));
         e = to_app(e)->get_arg(2);
     }