mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
94b4d1b442
commit
c629f09f21
|
@ -305,7 +305,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
if (m_euf) {
|
||||
convert_euf(t, root, sign);
|
||||
return;
|
||||
}
|
||||
}
|
||||
if (!is_uninterp_const(t)) {
|
||||
if (!is_app(t)) {
|
||||
std::ostringstream strm;
|
||||
|
@ -938,14 +938,10 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
}
|
||||
|
||||
void user_push() {
|
||||
push();
|
||||
force_push();
|
||||
}
|
||||
|
||||
void user_pop(unsigned n) {
|
||||
m_true = sat::null_literal;
|
||||
pop(n);
|
||||
|
||||
m_true = sat::null_literal;
|
||||
}
|
||||
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue