From 32fb679066e25071969419905f11477a78c7826e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 19 May 2015 11:01:15 +0100 Subject: [PATCH] tabs --- src/api/api_context.cpp | 2 +- src/ast/simplifier/inj_axiom.cpp | 2 +- src/cmd_context/interpolant_cmds.cpp | 10 +++--- src/duality/duality_rpfp.cpp | 16 +++++----- src/duality/duality_solver.cpp | 37 +++++++++++---------- src/duality/duality_wrapper.cpp | 2 +- src/interp/iz3base.cpp | 30 ++++++++--------- src/interp/iz3checker.cpp | 36 ++++++++++----------- src/interp/iz3interp.cpp | 48 ++++++++++++++-------------- src/interp/iz3pp.cpp | 6 ++-- src/interp/iz3proof_itp.cpp | 8 ++--- src/interp/iz3scopes.cpp | 4 +-- src/interp/iz3translate.cpp | 18 +++++------ src/interp/iz3translate_direct.cpp | 8 ++--- src/muz/base/dl_context.cpp | 12 +++---- src/shell/main.cpp | 2 +- src/util/mpz.cpp | 42 ++++++++++++------------ 17 files changed, 141 insertions(+), 142 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 846bab097..6e0c3cd82 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -89,7 +89,7 @@ namespace api { m_bv_util(m()), m_datalog_util(m()), m_fpa_util(m()), - m_dtutil(m()), + m_dtutil(m()), m_last_result(m()), m_ast_trail(m()), m_replay_stack() { diff --git a/src/ast/simplifier/inj_axiom.cpp b/src/ast/simplifier/inj_axiom.cpp index 50d051d2e..5925e23ac 100644 --- a/src/ast/simplifier/inj_axiom.cpp +++ b/src/ast/simplifier/inj_axiom.cpp @@ -114,7 +114,7 @@ bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) { ptr_vector domain; inv_vars.push_back(f); - for (unsigned i = 0; i < inv_vars.size(); ++i) { + for (unsigned i = 0; i < inv_vars.size(); ++i) { domain.push_back(m.get_sort(inv_vars[i])); } sort * d = decl->get_domain(idx); diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index f41f175ea..3add76030 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -36,11 +36,11 @@ #include"scoped_proof.h" static void show_interpolant_and_maybe_check(cmd_context & ctx, - ptr_vector &cnsts, - expr *t, - ptr_vector &interps, - params_ref &m_params, - bool check) + ptr_vector &cnsts, + expr *t, + ptr_vector &interps, + params_ref &m_params, + bool check) { if (m_params.get_bool("som", false)) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 0a3692295..897bc521f 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -1171,7 +1171,7 @@ namespace Duality { new_alits.push_back(conj); #endif slvr().add(ctx.make(Implies, res, conj)); - // std::cout << res << ": " << conj << "\n"; + // std::cout << res << ": " << conj << "\n"; } if (opt_map) (*opt_map)[res] = conj; @@ -2734,7 +2734,7 @@ namespace Duality { if(res != unsat) throw "should be unsat"; s.pop(1); - + for(unsigned i = 0; i < conjuncts.size(); ){ std::swap(conjuncts[i],conjuncts.back()); expr save = conjuncts.back(); @@ -3056,7 +3056,7 @@ namespace Duality { Push(); expr the_impl = is.get_implicant(); if(eq(the_impl,prev_impl)){ - // std::cout << "got old implicant\n"; + // std::cout << "got old implicant\n"; repeated_case_count++; } prev_impl = the_impl; @@ -3126,8 +3126,8 @@ namespace Duality { axioms_added = true; } else { - //#define KILL_ON_BAD_INTERPOLANT -#ifdef KILL_ON_BAD_INTERPOLANT + //#define KILL_ON_BAD_INTERPOLANT +#ifdef KILL_ON_BAD_INTERPOLANT std::cout << "bad in InterpolateByCase -- core:\n"; #if 0 std::vector assumps; @@ -3137,7 +3137,7 @@ namespace Duality { #endif std::cout << "checking for inconsistency\n"; std::cout << "model:\n"; - is.get_model().show(); + is.get_model().show(); expr impl = is.get_implicant(); std::vector conjuncts; CollectConjuncts(impl,conjuncts,true); @@ -3379,7 +3379,7 @@ namespace Duality { int arity = f.arity(); std::vector domain; for(int i = 0; i < arity; i++) - domain.push_back(f.domain(i)); + domain.push_back(f.domain(i)); return ctx.function(name.c_str(), arity, &domain[0], f.range()); } @@ -3390,7 +3390,7 @@ namespace Duality { int arity = f.arity(); std::vector domain; for(int i = 0; i < arity; i++) - domain.push_back(f.domain(i)); + domain.push_back(f.domain(i)); return ctx.function(name.c_str(), arity, &domain[0], f.range()); } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 1c441e5d2..4568ea913 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -55,7 +55,7 @@ // #define KEEP_EXPANSIONS // #define USE_CACHING_RPFP // #define PROPAGATE_BEFORE_CHECK -#define NEW_STRATIFIED_INLINING +#define NEW_STRATIFIED_INLINING #define USE_RPFP_CLONE #define USE_NEW_GEN_CANDS @@ -389,7 +389,7 @@ namespace Duality { else InstantiateAllEdges(); } else { -#ifdef NEW_STRATIFIED_INLINING +#ifdef NEW_STRATIFIED_INLINING #else CreateLeaves(); @@ -929,7 +929,7 @@ namespace Duality { int StratifiedLeafCount; -#ifdef NEW_STRATIFIED_INLINING +#ifdef NEW_STRATIFIED_INLINING /** Stratified inlining builds an initial layered unwinding before switching to the LAWI strategy. Currently the number of layers @@ -1135,7 +1135,6 @@ namespace Duality { conj = rpfp->conjoin(conjs); } } - Node *CreateUnderapproxNode(Node *node){ // cex.get_tree()->ComputeUnderapprox(cex.get_root(),0); @@ -1872,7 +1871,7 @@ namespace Duality { underapproximations as upper bounds. This mode is used to complete the partial derivation constructed in underapprox mode. - */ + */ bool Derive(RPFP *rpfp, RPFP::Node *root, bool _underapprox, bool _constrained = false, RPFP *_tree = 0){ underapprox = _underapprox; @@ -2066,7 +2065,7 @@ namespace Duality { if(!top->Outgoing || tree->Check(top,unused_set) == unsat){ unused_set.resize(orig_unused); if(to - from == 1){ -#if 1 +#if 1 std::cout << "Not using underapprox of " << used_set[from] ->number << std::endl; #endif choices.insert(used_set[from]); @@ -2250,14 +2249,14 @@ namespace Duality { throw "stacks out of sync!"; reporter->Depth(stack.size()); - // res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop + // res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop check_result foo = Check(); res = foo == unsat ? l_false : l_true; if (res == l_false) { if (stack.empty()) // should never happen return false; - + { std::vector &expansions = stack.back().expansions; int update_count = 0; @@ -2384,7 +2383,7 @@ namespace Duality { tree->Pop(1); node_order.clear(); while(stack.size() > 1){ - tree->Pop(1); + tree->Pop(1); std::vector &expansions = stack.back().expansions; for(unsigned i = 0; i < expansions.size(); i++) node_order.push_back(expansions[i]); @@ -2420,12 +2419,12 @@ namespace Duality { void PopLevel(){ std::vector &expansions = stack.back().expansions; - tree->Pop(1); + tree->Pop(1); hash_set leaves_to_remove; for(unsigned i = 0; i < expansions.size(); i++){ Node *node = expansions[i]; - // if(node != top) - // tree->ConstrainParent(node->Incoming[0],node); + // if(node != top) + //tree->ConstrainParent(node->Incoming[0],node); std::vector &cs = node->Outgoing->Children; for(unsigned i = 0; i < cs.size(); i++){ leaves_to_remove.insert(cs[i]); @@ -2441,7 +2440,7 @@ namespace Duality { } stack.pop_back(); } - + bool NodeTooComplicated(Node *node){ int ops = tree->CountOperators(node->Annotation.Formula); if(ops > 10) return true; @@ -2670,7 +2669,7 @@ namespace Duality { } } } -#endif +#endif } @@ -2732,7 +2731,7 @@ namespace Duality { return false; if(parent->underapprox_map.find(covering) != parent->underapprox_map.end()) return covering->number < covered->number || parent->underapprox_map[covering] == covered; -#endif +#endif return covering->number < covered->number; } @@ -2778,7 +2777,7 @@ namespace Duality { else return false; } -#endif +#endif bool Close(Node *node){ if(covered_by(node)) @@ -2842,7 +2841,7 @@ namespace Duality { #ifdef UNDERAPPROX_NODES // if(parent->underapprox_map.find(covering) != parent->underapprox_map.end()) // return parent->underapprox_map[covering] == covered; -#endif +#endif if(CoverOrder(covering,covered) && !IsCovered(covering)){ RPFP::Transformer f(covering->Annotation); f.SetEmpty(); @@ -3175,7 +3174,7 @@ namespace Duality { // else // std::cout << "constant not matched\n"; } - + RPFP *old_unwinding = old_solver->unwinding; hash_map > pred_match; @@ -3467,7 +3466,7 @@ namespace Duality { dnode->Bound.Formula = bound_fmla; } db_saved_bounds.push_back(bound_fmla); - // dnode->Annotation.Formula = ctx.make(And,node->Annotation.Formula,ctx.make(Geq,dvar,ctx.int_val(0))); + // dnode->Annotation.Formula = ctx.make(And,node->Annotation.Formula,ctx.make(Geq,dvar,ctx.int_val(0))); } for(unsigned i = 0; i < rpfp->edges.size(); i++){ Edge *edge = rpfp->edges[i]; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 0cb5df056..dc509d809 100755 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -727,7 +727,7 @@ namespace Duality { if(!started){ sw.start(); started = true; - } + } return sw.get_current_seconds(); } diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index bb4f760f5..57188e5ca 100755 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -292,14 +292,14 @@ bool iz3base::is_sat(const std::vector &q, ast &_proof, std::vector &v void iz3base::find_children(const stl_ext::hash_set &cnsts_set, - const ast &tree, - std::vector &cnsts, - std::vector &parents, - std::vector &conjuncts, - std::vector &children, - std::vector &pos_map, - bool merge - ){ + const ast &tree, + std::vector &cnsts, + std::vector &parents, + std::vector &conjuncts, + std::vector &children, + std::vector &pos_map, + bool merge + ){ std::vector my_children; std::vector my_conjuncts; if(op(tree) == Interp){ // if we've hit an interpolation position... @@ -336,13 +336,13 @@ void iz3base::find_children(const stl_ext::hash_set &cnsts_set, } void iz3base::to_parents_vec_representation(const std::vector &_cnsts, - const ast &tree, - std::vector &cnsts, - std::vector &parents, - std::vector &theory, - std::vector &pos_map, - bool merge - ){ + const ast &tree, + std::vector &cnsts, + std::vector &parents, + std::vector &theory, + std::vector &pos_map, + bool merge + ){ std::vector my_children; std::vector my_conjuncts; hash_set cnsts_set; diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp index 480e85274..69cfea8b8 100755 --- a/src/interp/iz3checker.cpp +++ b/src/interp/iz3checker.cpp @@ -144,7 +144,7 @@ struct iz3checker : iz3base { hash_set tmemo; for(unsigned j = 0; j < theory.size(); j++) support(theory[j],common,tmemo); // all theory symbols allowed in interps - } + } hash_set memo; support(itp[i],Isup,memo); std::set_difference(Isup.begin(),Isup.end(),common.begin(),common.end(),std::inserter(bad,bad.begin())); @@ -192,35 +192,35 @@ std::vector to_std_vector(const ::vector &v){ bool iz3check(ast_manager &_m_manager, - solver *s, - std::ostream &err, - const ptr_vector &cnsts, - const ::vector &parents, - const ptr_vector &interps, - const ptr_vector &theory) + solver *s, + std::ostream &err, + const ptr_vector &cnsts, + const ::vector &parents, + const ptr_vector &interps, + const ptr_vector &theory) { iz3checker chk(_m_manager); return chk.check(s,err,chk.cook(cnsts),to_std_vector(parents),chk.cook(interps),chk.cook(theory)); } bool iz3check(iz3mgr &mgr, - solver *s, - std::ostream &err, - const std::vector &cnsts, - const std::vector &parents, - const std::vector &interps, - const std::vector &theory) + solver *s, + std::ostream &err, + const std::vector &cnsts, + const std::vector &parents, + const std::vector &interps, + const std::vector &theory) { iz3checker chk(mgr); return chk.check(s,err,cnsts,parents,interps,theory); } bool iz3check(ast_manager &_m_manager, - solver *s, - std::ostream &err, - const ptr_vector &_cnsts, - ast *tree, - const ptr_vector &interps) + solver *s, + std::ostream &err, + const ptr_vector &_cnsts, + ast *tree, + const ptr_vector &interps) { iz3checker chk(_m_manager); return chk.check(s,err,chk.cook(_cnsts),chk.cook(tree),chk.cook(interps)); diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index c9b5e7920..810afb103 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -252,7 +252,7 @@ public: // create a secondary prover iz3secondary *sp = iz3foci::create(this,num,parents_vec.empty()?0:&parents_vec[0]); sp_killer.set(sp); // kill this on exit - + #define BINARY_INTERPOLATION #ifndef BINARY_INTERPOLATION // create a translator @@ -420,12 +420,12 @@ public: void iz3interpolate(ast_manager &_m_manager, - ast *proof, - const ptr_vector &cnsts, - const ::vector &parents, - ptr_vector &interps, - const ptr_vector &theory, - interpolation_options_struct * options) + ast *proof, + const ptr_vector &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector &theory, + interpolation_options_struct * options) { iz3interp itp(_m_manager); if(options) @@ -448,12 +448,12 @@ void iz3interpolate(ast_manager &_m_manager, } void iz3interpolate(ast_manager &_m_manager, - ast *proof, - const ::vector > &cnsts, - const ::vector &parents, - ptr_vector &interps, - const ptr_vector &theory, - interpolation_options_struct * options) + ast *proof, + const ::vector > &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector &theory, + interpolation_options_struct * options) { iz3interp itp(_m_manager); if(options) @@ -477,11 +477,11 @@ void iz3interpolate(ast_manager &_m_manager, } void iz3interpolate(ast_manager &_m_manager, - ast *proof, - const ptr_vector &cnsts, - ast *tree, - ptr_vector &interps, - interpolation_options_struct * options) + ast *proof, + const ptr_vector &cnsts, + ast *tree, + ptr_vector &interps, + interpolation_options_struct * options) { iz3interp itp(_m_manager); if(options) @@ -506,12 +506,12 @@ void iz3interpolate(ast_manager &_m_manager, } lbool iz3interpolate(ast_manager &_m_manager, - solver &s, - ast *tree, - ptr_vector &cnsts, - ptr_vector &interps, - model_ref &m, - interpolation_options_struct * options) + solver &s, + ast *tree, + ptr_vector &cnsts, + ptr_vector &interps, + model_ref &m, + interpolation_options_struct * options) { iz3interp itp(_m_manager); if(options) diff --git a/src/interp/iz3pp.cpp b/src/interp/iz3pp.cpp index 26cefedb3..066e04e83 100644 --- a/src/interp/iz3pp.cpp +++ b/src/interp/iz3pp.cpp @@ -107,9 +107,9 @@ public: }; void iz3pp(ast_manager &m, - const ptr_vector &cnsts_vec, - expr *tree, - std::ostream& out) { + const ptr_vector &cnsts_vec, + expr *tree, + std::ostream& out) { unsigned sz = cnsts_vec.size(); expr* const* cnsts = &cnsts_vec[0]; diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 0bdd51ed8..f76de14cf 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -778,7 +778,7 @@ class iz3proof_itp_impl : public iz3proof_itp { sum_cond_ineq(ineq2,make_int("1"),yleqx,Aproves2,Bproves2); ast Bcond = my_implies(Bproves1,my_and(Aproves1,z3_simplify(ineq2))); // if(!is_true(Aproves1) || !is_true(Bproves1)) - // std::cout << "foo!\n";; + // std::cout << "foo!\n";; if(y == make_int(rational(0)) && op(x) == Plus && num_args(x) == 2){ if(get_term_type(arg(x,0)) == LitA){ ast iter = z3_simplify(make(Plus,arg(x,0),get_ineq_rhs(xleqy))); @@ -915,7 +915,7 @@ class iz3proof_itp_impl : public iz3proof_itp { int ipos = pos.get_unsigned(); ast cond = mk_true(); ast equa = sep_cond(arg(pf,0),cond); -#if 0 +#if 0 if(op(equa) == Equal){ ast pe = mk_not(neg_equality); ast lhs = subst_in_arg_pos(ipos,arg(equa,0),arg(pe,0)); @@ -2784,7 +2784,7 @@ class iz3proof_itp_impl : public iz3proof_itp { } else if(o == Plus || o == Times){ // don't want bound variables inside arith ops // std::cout << "WARNING: non-local arithmetic\n"; - // frng = erng; // this term will be localized + // frng = erng; // this term will be localized } else if(o == Select){ // treat the array term like a function symbol prover::range srng = pv->ast_scope(arg(e,0)); @@ -2805,7 +2805,7 @@ class iz3proof_itp_impl : public iz3proof_itp { pfs.push_back(argpf); } } - + e = clone(e,largs); if(pfs.size()) pf = make_congruence(eqs,make_equiv(e,orig_e),pfs); diff --git a/src/interp/iz3scopes.cpp b/src/interp/iz3scopes.cpp index c365619b2..b70f37a06 100755 --- a/src/interp/iz3scopes.cpp +++ b/src/interp/iz3scopes.cpp @@ -97,7 +97,7 @@ namespace std { template <> inline size_t stdext::hash_value(const scopes::range_lo& p) -{ +{ std::hash h; return h(p); } @@ -133,7 +133,7 @@ namespace std { template <> inline size_t stdext::hash_value(const range_op& p) -{ +{ std::hash h; return h(p); } diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 5b420673c..e4bccace1 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -274,7 +274,7 @@ public: ast neglit = mk_not(arg(con,i)); res.erase(neglit); } - } + } } } #if 0 @@ -612,7 +612,7 @@ public: rng = range_glb(rng,ast_scope(lit)); } if(range_is_empty(rng)) return -1; - int hi = range_max(rng); + int hi = range_max(rng); if(hi >= frames) return frames - 1; return hi; } @@ -2003,10 +2003,10 @@ public: } iz3translation_full(iz3mgr &mgr, - iz3secondary *_secondary, + iz3secondary *_secondary, const std::vector > &cnsts, - const std::vector &parents, - const std::vector &theory) + const std::vector &parents, + const std::vector &theory) : iz3translation(mgr, cnsts, parents, theory) { frames = cnsts.size(); @@ -2027,10 +2027,10 @@ public: #ifdef IZ3_TRANSLATE_FULL iz3translation *iz3translation::create(iz3mgr &mgr, - iz3secondary *secondary, - const std::vector > &cnsts, - const std::vector &parents, - const std::vector &theory){ + iz3secondary *secondary, + const std::vector > &cnsts, + const std::vector &parents, + const std::vector &theory){ return new iz3translation_full(mgr,secondary,cnsts,parents,theory); } diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index c1b751c6f..ec3af1ca3 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -293,7 +293,7 @@ public: ast neglit = mk_not(arg(con,i)); res.erase(neglit); } - } + } } } #if 0 @@ -589,7 +589,7 @@ public: rng = range_glb(rng,ast_scope(lit)); } if(range_is_empty(rng)) return -1; - int hi = range_max(rng); + int hi = range_max(rng); if(hi >= frames) return frames - 1; return hi; } @@ -881,7 +881,7 @@ public: || dk == PR_QUANT_INST //|| dk == PR_UNIT_RESOLUTION //|| dk == PR_LEMMA - ) + ) return false; if(dk == PR_HYPOTHESIS && hyps.find(con) != hyps.end()) ; //std::cout << "blif!\n"; @@ -1481,7 +1481,7 @@ public: AstSet dummy; collect_resolvent_lits(nll->proofs[i],dummy,reslits); litset.insert(reslits.begin(),reslits.end()); - } + } } if(to_keep.size() == nll->proofs.size()) return nll; ResolventAppSet new_proofs; diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index a2ab3610a..b7cb5680f 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -584,7 +584,7 @@ namespace datalog { m_rule_properties.check_existential_tail(); m_rule_properties.check_for_negated_predicates(); break; - case DUALITY_ENGINE: + case DUALITY_ENGINE: m_rule_properties.collect(r); m_rule_properties.check_existential_tail(); m_rule_properties.check_for_negated_predicates(); @@ -986,12 +986,12 @@ namespace datalog { } } - void context::get_raw_rule_formulas(expr_ref_vector& rules, svector& names, vector &bounds){ + void context::get_raw_rule_formulas(expr_ref_vector& rules, svector& names, vector &bounds) { for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { - expr_ref r = bind_vars(m_rule_fmls[i].get(), true); - rules.push_back(r.get()); - names.push_back(m_rule_names[i]); - bounds.push_back(m_rule_bounds[i]); + expr_ref r = bind_vars(m_rule_fmls[i].get(), true); + rules.push_back(r.get()); + names.push_back(m_rule_names[i]); + bounds.push_back(m_rule_bounds[i]); } } diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 2dbd459fa..5a47d0d16 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -329,7 +329,7 @@ int main(int argc, char ** argv) { g_input_kind = IN_SMTLIB; } } - } + } switch (g_input_kind) { case IN_SMTLIB: return_value = read_smtlib_file(g_input_file); diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 163f7fb86..855927919 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -336,17 +336,17 @@ void mpz_manager::set(mpz & target, unsigned sz, digit_t const * digits) } } #else - mk_big(target); - // reset - mpz_set_ui(*target.m_ptr, digits[sz - 1]); - SASSERT(sz > 0); - unsigned i = sz - 1; - while (i > 0) { - --i; - mpz_mul_2exp(*target.m_ptr, *target.m_ptr, 32); - mpz_set_ui(m_tmp, digits[i]); - mpz_add(*target.m_ptr, *target.m_ptr, m_tmp); - } + mk_big(target); + // reset + mpz_set_ui(*target.m_ptr, digits[sz - 1]); + SASSERT(sz > 0); + unsigned i = sz - 1; + while (i > 0) { + --i; + mpz_mul_2exp(*target.m_ptr, *target.m_ptr, 32); + mpz_set_ui(m_tmp, digits[i]); + mpz_add(*target.m_ptr, *target.m_ptr, m_tmp); + } #endif } } @@ -2037,16 +2037,16 @@ bool mpz_manager::decompose(mpz const & a, svector & digits) { } return a.m_val < 0; #else - bool r = is_neg(a); - mpz_set(m_tmp, *a.m_ptr); - mpz_abs(m_tmp, m_tmp); - while (mpz_sgn(m_tmp) != 0) { - mpz_tdiv_r_2exp(m_tmp2, m_tmp, 32); - unsigned v = mpz_get_ui(m_tmp2); - digits.push_back(v); - mpz_tdiv_q_2exp(m_tmp, m_tmp, 32); - } - return r; + bool r = is_neg(a); + mpz_set(m_tmp, *a.m_ptr); + mpz_abs(m_tmp, m_tmp); + while (mpz_sgn(m_tmp) != 0) { + mpz_tdiv_r_2exp(m_tmp2, m_tmp, 32); + unsigned v = mpz_get_ui(m_tmp2); + digits.push_back(v); + mpz_tdiv_q_2exp(m_tmp, m_tmp, 32); + } + return r; #endif } }