mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

fix #3260

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-13 11:42:25 -07:00
parent d530d1314b
commit 59755dd72e
1 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_utvpi_def.h
View file

@ -546,8 +546,9 @@ namespace smt {
// do not create an alias. // do not create an alias.
return null_theory_var; return null_theory_var;
} }
for (unsigned i = 0; i < n->get_num_args(); ++i) { for (expr* arg : *n) {
mk_term(to_app(n->get_arg(i))); if (!ctx.e_internalized(arg))
ctx.internalize(arg, false);
} }
th_var target = mk_var(ctx.mk_enode(n, false, false, true)); th_var target = mk_var(ctx.mk_enode(n, false, false, true));
coeffs.push_back(std::make_pair(target, rational(-1))); coeffs.push_back(std::make_pair(target, rational(-1)));
@ -571,6 +572,10 @@ namespace smt {
SASSERT(v != null_theory_var); SASSERT(v != null_theory_var);
} }
else { else {
for (expr* arg : *n) {
if (!ctx.e_internalized(arg))
ctx.internalize(arg, false);
}
v = mk_var(ctx.mk_enode(n, false, false, true)); v = mk_var(ctx.mk_enode(n, false, false, true));
// v = k: v <= k k <= v // v = k: v <= k k <= v
coeffs coeffs; coeffs coeffs;