diff options
author | Guy <katz911@gmail.com> | 2016-08-03 15:51:22 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-08-03 15:51:22 -0700 |
commit | c82514b57252444df982b35af4809e0fd4635e37 (patch) | |
tree | 12ad1fe87c8d7723762a120645006bed29ce8c51 /src/proof/array_proof.cpp | |
parent | 53020abb9381f4e29d628c054c990ddb43bba4b2 (diff) |
Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.
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; |