mirror of
https://github.com/Z3Prover/z3
synced 2025-08-07 03:31:23 +00:00
This commit is contained in:
parent
9989ef6553
commit
b1002638ab
1 changed files with 1 additions and 1 deletions
|
@ -436,8 +436,8 @@ namespace arith {
|
||||||
theory_var v = mk_evar(t);
|
theory_var v = mk_evar(t);
|
||||||
if (_has_var)
|
if (_has_var)
|
||||||
return v;
|
return v;
|
||||||
theory_var w = mk_evar(n);
|
|
||||||
internalize_term(n);
|
internalize_term(n);
|
||||||
|
theory_var w = mk_evar(n);
|
||||||
|
|
||||||
if (p == 0) {
|
if (p == 0) {
|
||||||
mk_power0_axioms(t, n);
|
mk_power0_axioms(t, n);
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue