mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

rename repeated class apart

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-24 09:03:28 -07:00
parent 2c3b56315d
commit 1315c8d7de
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/muz/base/proof_utils.cpp
View file

@ -9,7 +9,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
class reduce_hypotheses { class reduce_hypotheses0 {
typedef obj_hashtable<expr> expr_set; typedef obj_hashtable<expr> expr_set;
ast_manager& m; ast_manager& m;
// reference for any expression created by the tranformation // reference for any expression created by the tranformation
@ -137,7 +137,7 @@ class reduce_hypotheses {
} }
public: public:
reduce_hypotheses(ast_manager& m): m(m), m_refs(m) {} reduce_hypotheses0(ast_manager& m): m(m), m_refs(m) {}
void operator()(proof_ref& pr) { void operator()(proof_ref& pr) {
proof_ref tmp(m); proof_ref tmp(m);
@ -416,7 +416,7 @@ public:
void proof_utils::reduce_hypotheses(proof_ref& pr) { void proof_utils::reduce_hypotheses(proof_ref& pr) {
ast_manager& m = pr.get_manager(); ast_manager& m = pr.get_manager();
class reduce_hypotheses reduce(m); class reduce_hypotheses0 reduce(m);
reduce(pr); reduce(pr);
CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";); CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";);
} }