diff options
Diffstat (limited to 'src/proof/array_proof.cpp')
-rw-r--r-- | src/proof/array_proof.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index ccc072eca..514d81184 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -1324,6 +1324,7 @@ void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren printSort(array_type.getConstituentType(), os); os << "))\n"; + paren << ")"; } else { Assert(term.isVariable()); if (ProofManager::getSkolemizationManager()->isSkolem(*it)) { @@ -1333,10 +1334,9 @@ void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren os << "(% " << ProofManager::sanitize(term) << " "; os << "(term "; os << term.getType() << ")\n"; + paren << ")"; } } - - paren << ")"; } Debug("pf::array") << "Declaring terms done!" << std::endl; |