From a5e3713c2c5e1065510d927a9c07ab240b3bf870 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Jun 2014 05:47:42 -0700 Subject: [PATCH] fix unmatched parenthsis and code odor Signed-off-by: Nikolaj Bjorner --- examples/tptp/tptp5.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index d0e174914..00d03a8b0 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -1630,10 +1630,8 @@ public: unsigned parent_id = Z3_get_ast_id(ctx, p.arg(0)); std::set const& hyps = m_proof_hypotheses.find(parent_id)->second; print_hypotheses(out, hyps); - out << ").\n"; + out << "))).\n"; break; - display_inference(out, "lemma", "thm", p); - break; } case Z3_OP_PR_UNIT_RESOLUTION: display_inference(out, "unit_resolution", "thm", p);