Theorem: BVDecide.unsat_of_verifyBVExpr_eq_true (LeanSAT/Reflect/Tactics/BVDecide.lean)

State before:
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.unsat
Tactic:
apply BVLogicalExpr.unsat_of_bitblast
State after:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.bitblast.unsat

State before:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.bitblast.unsat
Tactic:
rw [← AIG.Entrypoint.relabelNat_unsat_iff]
State after:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.bitblast.relabelNat.unsat

State before:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.bitblast.relabelNat.unsat
Tactic:
rw [← AIG.toCNF_equisat]
State after:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ (AIG.toCNF bv.bitblast.relabelNat).unsat

State before:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ (AIG.toCNF bv.bitblast.relabelNat).unsat
Tactic:
apply verifyCert_correct
State after:
case a.a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ LratCert

State before:
case a.a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ LratCert
Tactic:
rw [verifyBVExpr] at h
State after:
case a.a
bv : BVLogicalExpr
c : LratCert
h✝ : verifyBVExpr bv c = true
h : verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) c = true
⊢ verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ LratCert

State before:
case a.a
bv : BVLogicalExpr
c : LratCert
h✝ : verifyBVExpr bv c = true
h : verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) c = true
⊢ verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ LratCert
Tactic:
assumption
State after:
no goals