mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
also add separate cut rule
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
68a437e615
commit
423a7b6888
|
@ -255,7 +255,6 @@ namespace euf {
|
|||
smt_proof_hint* solver::mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne, expr_pair const* eqs, unsigned nd, expr_pair const* deqs) {
|
||||
if (!use_drat())
|
||||
return nullptr;
|
||||
TRACE("euf", tout << "SMT hint " << n << "\n");
|
||||
push(value_trail(m_lit_tail));
|
||||
push(restore_vector(m_proof_literals));
|
||||
|
||||
|
|
Loading…
Reference in a new issue