diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 31ab1bb19..2312f4389 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -184,7 +184,7 @@ typedef enum Z3_PARAMETER_SYMBOL, Z3_PARAMETER_SORT, Z3_PARAMETER_AST, - Z3_PARAMETER_FUNC_DECL, + Z3_PARAMETER_FUNC_DECL } Z3_parameter_kind; /** diff --git a/src/ast/ast.h b/src/ast/ast.h index 32a5c78ba..8547675a8 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1146,7 +1146,7 @@ typedef app proof; /* a proof is just an applicaton */ enum label_op_kind { OP_LABEL, - OP_LABEL_LIT, + OP_LABEL_LIT }; /** diff --git a/src/ast/pattern/expr_pattern_match.h b/src/ast/pattern/expr_pattern_match.h index c3c0256fd..245edd877 100644 --- a/src/ast/pattern/expr_pattern_match.h +++ b/src/ast/pattern/expr_pattern_match.h @@ -37,7 +37,7 @@ class expr_pattern_match { CHECK_TERM, SET_BOUND, CHECK_BOUND, - YIELD, + YIELD }; struct instr { diff --git a/src/smt/params/dyn_ack_params.cpp b/src/smt/params/dyn_ack_params.cpp index c559e2b9b..15f48bad1 100644 --- a/src/smt/params/dyn_ack_params.cpp +++ b/src/smt/params/dyn_ack_params.cpp @@ -27,4 +27,4 @@ void dyn_ack_params::updt_params(params_ref const & _p) { m_dack_threshold = p.dack_threshold(); m_dack_gc = p.dack_gc(); m_dack_gc_inv_decay = p.dack_gc_inv_decay(); -} \ No newline at end of file +} diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 2c1ac13c5..8127b7eef 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -66,7 +66,7 @@ enum case_split_strategy { CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity CS_RELEVANCY, // case split based on relevancy CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity - CS_RELEVANCY_GOAL, // based on relevancy and the current goal + CS_RELEVANCY_GOAL // based on relevancy and the current goal }; struct smt_params : public preprocessor_params, diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 679fd473f..68cd5703c 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -28,7 +28,7 @@ namespace smt { enum config_mode { CFG_BASIC, // install theories based on user options CFG_LOGIC, // install theories and configure Z3 based on the value of the parameter set-logic. - CFG_AUTO, // install theories based on static features of the input formula + CFG_AUTO // install theories based on static features of the input formula }; class context; diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 4cce4bfd1..a6ae73eb8 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -108,4 +108,4 @@ model_converter * mk_fpa2bv_model_converter(ast_manager & m, obj_map const & uf2bvuf, obj_hashtable const & m_decls_to_hide); -#endif \ No newline at end of file +#endif diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 33b6c15b9..59b9fd7a5 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -820,4 +820,4 @@ public: } }; -#endif \ No newline at end of file +#endif diff --git a/src/tactic/sls/sls_powers.h b/src/tactic/sls/sls_powers.h index c514fec00..b632e7100 100644 --- a/src/tactic/sls/sls_powers.h +++ b/src/tactic/sls/sls_powers.h @@ -46,4 +46,4 @@ public: } }; -#endif \ No newline at end of file +#endif diff --git a/src/util/hwf.h b/src/util/hwf.h index d2055d56e..cf0c9b7ea 100644 --- a/src/util/hwf.h +++ b/src/util/hwf.h @@ -127,15 +127,15 @@ public: void to_rational(hwf const & x, scoped_mpq & o) { to_rational(x, o.m(), o); } - bool sgn(hwf const & x) const { + bool sgn(hwf const & x) const { return (x.get_raw() & 0x8000000000000000ull) != 0; } - uint64 sig(hwf const & x) const { + uint64 sig(hwf const & x) const { return x.get_raw() & 0x000FFFFFFFFFFFFFull; } - int exp(hwf const & x) const { + int exp(hwf const & x) const { return ((x.get_raw() & 0x7FF0000000000000ull) >> 52) - 1023; }