pub fn lower_bool(e: &BoundedExpr) -> Option<ProofExpr>Expand description
Lower a boolean-VALUED datapath comparison to a ProofExpr, or None if unsupported.
Comparisons over bitvectors are unsigned unless the op is explicitly signed (SLt).
pub fn lower_bool(e: &BoundedExpr) -> Option<ProofExpr>Lower a boolean-VALUED datapath comparison to a ProofExpr, or None if unsupported.
Comparisons over bitvectors are unsigned unless the op is explicitly signed (SLt).