mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
This commit is contained in:
parent
d50c4bfcc1
commit
1e9e52a58f
|
@ -308,7 +308,6 @@ namespace arith {
|
|||
|
||||
bool solver::internalize_atom(expr* atom) {
|
||||
TRACE("arith", tout << mk_pp(atom, m) << "\n";);
|
||||
SASSERT(!ctx.get_enode(atom));
|
||||
expr* n1, *n2;
|
||||
rational r;
|
||||
lp_api::bound_kind k;
|
||||
|
|
Loading…
Reference in a new issue