From 392266c278c3b1ca21a89610e8a731c40a41bca2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 May 2023 12:16:58 -0700 Subject: [PATCH] fix processing of else expression for model table --- src/model/func_interp.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index b180a8a1f..ebb22f079 100644 --- 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 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); }