use right arith explanation fn to fix regressions (#5231)
authorAlex Ozdemir <aozdemir@hmc.edu>
Fri, 9 Oct 2020 17:48:16 +0000 (10:48 -0700)
committerGitHub <noreply@github.com>
Fri, 9 Oct 2020 17:48:16 +0000 (12:48 -0500)
commita078e193eb13e398f663eff2d0b9a2ef145ca75f
treeb8171fdc29e54a831a7d2eeca1aed6e556871734
parent5fd55819da2ea6fdf0472f2e212330d09c4b5317
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