diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-02-10 18:32:20 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-10 18:32:20 -0800 |
| commit | cbf99fdd92c483e70e3b73feb9d368d4bf632a24 (patch) | |
| tree | cfa26fae871b0d3912d2721a39e5429b955c581a /src/proof/theory_proof.cpp | |
| parent | 499f1c70dbc869e2b1dd5f8a7b98d45bee2d29cc (diff) | |
Implement LFSCArithProof::equalityType. (#3740)
Also, missed an armType use.
Diffstat (limited to 'src/proof/theory_proof.cpp')
| -rw-r--r-- | src/proof/theory_proof.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index b516c250f..88a53062a 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -971,7 +971,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, } else { - printBoundTerm(term[2], os, map); + printBoundTerm(term[2], os, map, armType); } os << ")"; return; |