Searched refs:bvUDivConst (Results 1 – 4 of 4) sorted by relevance
488 virtual Theorem bvUDivConst(const Expr& divExpr) = 0;
576 virtual Theorem bvUDivConst(const Expr& divExpr);
1461 res = d_rules->bvUDivConst(e); in rewriteBV()
6243 Theorem BitvectorTheoremProducer::bvUDivConst(const Expr& divExpr) in bvUDivConst() function in BitvectorTheoremProducer