diff options
Diffstat (limited to 'src/theory/arith/proof_checker.cpp')
-rw-r--r-- | src/theory/arith/proof_checker.cpp | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index 4e25ae76b..58de8e391 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -36,11 +36,8 @@ void ArithProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::INT_TIGHT_UB, this); pc->registerChecker(PfRule::INT_TIGHT_LB, this); pc->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM, this); - pc->registerChecker(PfRule::ARITH_MULT_POS, this); pc->registerChecker(PfRule::ARITH_MULT_NEG, this); - // trusted rules - pc->registerTrustedChecker(PfRule::INT_TRUST, this, 2); } Node ArithProofRuleChecker::checkInternal(PfRule id, @@ -340,25 +337,6 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, } // Check that all have the same constant: } - case PfRule::INT_TRUST: - { - if (Debug.isOn("arith::pf::check::trust")) - { - Debug("arith::pf::check::trust") << "Arith PfRule:" << id << std::endl; - Debug("arith::pf::check::trust") << " children: " << std::endl; - for (const auto& c : children) - { - Debug("arith::pf::check::trust") << " * " << c << std::endl; - } - Debug("arith::pf::check::trust") << " args:" << std::endl; - for (const auto& c : args) - { - Debug("arith::pf::check::trust") << " * " << c << std::endl; - } - } - Assert(args.size() == 1); - return args[0]; - } case PfRule::ARITH_OP_ELIM_AXIOM: { Assert(children.empty()); |