search

cvc5 / cvc5-projects

1 stars 0 forks source link

Closed proof issue on regress1/nl/factor_agg_s.smt2 #313

Closed ajreynol closed 3 years ago

ajreynol commented 3 years ago

cvc5 regress1/nl/factor_agg_s.smt2 --check-proofs --proof-check=eager --decision=justification

generates:

Fatal failure within void cvc5::ensureClosedWrtInternal(cvc5::Node, cvc5::ProofGenerator, cvc5::ProofNode, const std::vector<cvc5::NodeTemplate >&, const char, const char, bool) at /space/ajreynol/cvc5-ajr/src/proof/proof_ensure_closed.cpp:140 Check failure

isClosed ...ensureClosed: open proof from ProofGenerator: Proof_0 in context TheoryEngine::lemma_initial, use -t te-proof-debug for details, use -t dump-proof-error for details on proof Abort (core dumped)

ajreynol commented 3 years ago

Appears to be a open proof of a theory lemma from the NL solver.