mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
67bbdc7524
commit
260f759177
|
@ -384,7 +384,7 @@ class theory_lra::imp {
|
|||
vars.push_back(v);
|
||||
++index;
|
||||
}
|
||||
else if(a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r <= 10) {
|
||||
else if (a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r <= 10) {
|
||||
theory_var v = internalize_power(to_app(n), to_app(n1), r.get_unsigned());
|
||||
coeffs[vars.size()] = coeffs[index];
|
||||
vars.push_back(v);
|
||||
|
@ -510,6 +510,7 @@ class theory_lra::imp {
|
|||
theory_var v = mk_var(t);
|
||||
if (_has_var)
|
||||
return v;
|
||||
VERIFY(internalize_term(n));
|
||||
theory_var w = mk_var(n);
|
||||
svector<lpvar> vars;
|
||||
for (unsigned i = 0; i < p; ++i)
|
||||
|
|
Loading…
Reference in a new issue