mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

fix #2803

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-29 21:29:39 -08:00
parent 0f772482b8
commit 3b16f129bb
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_recfun.cpp
View file

@ -75,6 +75,9 @@ namespace smt {
bool_var v = ctx().mk_bool_var(atom); bool_var v = ctx().mk_bool_var(atom);
ctx().set_var_theory(v, get_id()); ctx().set_var_theory(v, get_id());
} }
if (!ctx().relevancy() && u().is_defined(atom)) {
push_case_expand(alloc(case_expansion, u(), atom));
}
return true; return true;
} }