Theorem: BVLogicalExpr.unsat_of_bitblast (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas.lean)

State before:
expr : BVLogicalExpr
⊢ expr.bitblast.unsat → expr.unsat
Tactic:
intro h assign
State after:
expr : BVLogicalExpr
h : expr.bitblast.unsat
assign : BVExpr.Assignment
⊢ eval assign expr = false

State before:
expr : BVLogicalExpr
h : expr.bitblast.unsat
assign : BVExpr.Assignment
⊢ eval assign expr = false
Tactic:
rw [← bitblast_denote_eq_eval]
State after:
expr : BVLogicalExpr
h : expr.bitblast.unsat
assign : BVExpr.Assignment
⊢ ⟦expr.bitblast, assign.toAIGAssignment⟧ = false

State before:
expr : BVLogicalExpr
h : expr.bitblast.unsat
assign : BVExpr.Assignment
⊢ ⟦expr.bitblast, assign.toAIGAssignment⟧ = false
Tactic:
apply h
State after:
no goals