pub fn test_concrete_with_static_widths( rulectx: &RuleCtx<'_>, concrete: &ConcreteTest, lhs: SExpr, rhs: SExpr, ctx: &mut SolverCtx, assumptions: Vec<SExpr>, ) -> VerificationResult