diff options
Diffstat (limited to 'src/smt/proof_manager.cpp')
| -rw-r--r-- | src/smt/proof_manager.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 53633a123..0968aa1f9 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -66,6 +66,7 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte) d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_TRANSFORM); d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION_TRUST); d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION); + d_pfpp->setEliminateRule(PfRule::MACRO_ARITH_SCALE_SUM_UB); if (options::proofGranularityMode() != options::ProofGranularityMode::REWRITE) { |