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