1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index d8fc1c578..03db36bb5 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -29,6 +29,7 @@
 #include "theory/arith/congruence_manager.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/partial_model.h"
+#include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
 
 using namespace std;
@@ -1820,9 +1821,11 @@ std::shared_ptr<ProofNode> Constraint::externalExplain(
         }
         case ArithProofType::IntHoleAP:
         {
-          pf = pnm->mkNode(PfRule::INT_TRUST,
+          Node t =
+              builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH);
+          pf = pnm->mkNode(PfRule::THEORY_INFERENCE,
                            children,
-                           {getProofLiteral()},
+                           {getProofLiteral(), t},
                            getProofLiteral());
           break;
         }