From a078e193eb13e398f663eff2d0b9a2ef145ca75f Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Fri, 9 Oct 2020 10:48:16 -0700
Subject: [PATCH] use right arith explanation fn to fix regressions (#5231)

Use the Node-returning variants of
Constraint::externalExplainByAssertions in TheoryArithPrivate locations
that aren't computing proofs.

The problem is that the TrustNode returning variant requires that arith
has stored an externally valid literal for the constraint, which is not
always the case.

This is what we did on proof-new, I just forgot.
---
 src/theory/arith/theory_arith_private.cpp | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 760d98b1b..3abd9495e 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1632,9 +1632,9 @@ Node TheoryArithPrivate::callDioSolver(){
 
     Node orig = Node::null();
     if(lb->isEquality()){
-      orig = lb->externalExplainByAssertions().getNode();
+      orig = Constraint::externalExplainByAssertions({lb});
     }else if(ub->isEquality()){
-      orig = ub->externalExplainByAssertions().getNode();
+      orig = Constraint::externalExplainByAssertions({ub});
     }else {
       orig = Constraint::externalExplainByAssertions(ub, lb);
     }
@@ -1706,7 +1706,9 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(TNode assertion)
     Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
     constraint->setAssumption(inConflict);
   } else {
-    Debug("arith::constraint") << "already has proof: " << constraint->externalExplainByAssertions() << endl;
+    Debug("arith::constraint")
+        << "already has proof: "
+        << Constraint::externalExplainByAssertions({constraint});
   }
 
   if(Debug.isOn("arith::negatedassumption") && inConflict){
@@ -5006,7 +5008,7 @@ void TheoryArithPrivate::entailmentCheckBoundLookup(std::pair<Node, DeltaRationa
       ? d_partialModel.getUpperBoundConstraint(v)
       : d_partialModel.getLowerBoundConstraint(v);
     if(c != NullConstraint){
-      tmp.first = c->externalExplainByAssertions().getNode();
+      tmp.first = Constraint::externalExplainByAssertions({c});
       tmp.second = c->getValue();
     }
   }
-- 
2.30.2