mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

fix processing of else expression for model table

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-05-02 12:16:58 -07:00
parent d5231f8b33
commit 392266c278
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/model/func_interp.cpp
View file

@ -146,6 +146,7 @@ void func_interp::set_else(expr * e) {
ptr_vector<expr> args; ptr_vector<expr> args;
while (e && is_fi_entry_expr(e, args)) { while (e && is_fi_entry_expr(e, args)) {
if (!get_entry(args.data()))
insert_entry(args.data(), to_app(e)->get_arg(1)); insert_entry(args.data(), to_app(e)->get_arg(1));
e = to_app(e)->get_arg(2); e = to_app(e)->get_arg(2);
} }