mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Bugfix for unspecified else-case in func_interps.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-04-06 15:39:32 +01:00
parent 7534b53bae
commit e527aca296
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/model/func_interp.cpp
View file

@ -145,7 +145,7 @@ void func_interp::set_else(expr * e) {
m_manager.dec_ref(m_else);
ptr_vector<expr> args;
while (is_fi_entry_expr(e, args)) {
while (e && is_fi_entry_expr(e, args)) {
TRACE("func_interp", tout << "fi entry expr: " << mk_ismt2_pp(e, m()) << std::endl;);
insert_entry(args.c_ptr(), to_app(e)->get_arg(1));
e = to_app(e)->get_arg(2);