mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix unmatched parenthsis and code odor

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-06-14 05:47:42 -07:00
parent 8ef4ec7009
commit a5e3713c2c
1 changed files with 1 additions and 3 deletions

4
examples/tptp/tptp5.cpp
View file

@ -1630,10 +1630,8 @@ public:
unsigned parent_id = Z3_get_ast_id(ctx, p.arg(0));
std::set<unsigned> 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);