mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

compile warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-02-19 10:03:38 -08:00
parent 6352340478
commit 9b6ac45e02
3 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/test/interval.cpp
View file

@ -200,14 +200,12 @@ static void mk_random_interval(T & cfg, interval & a, unsigned magnitude) {
#define BUFFER_SZ 256 #define BUFFER_SZ 256
static int g_problem_id = 0; static int g_problem_id = 0;
static char g_buffer[BUFFER_SZ];
static std::stringstream ous;
char const * get_next_file_name() { std::string get_next_file_name() {
ous.clear(); std::stringstream ous;
ous << "interval_lemma_" << g_problem_id << ".smt2"; ous << "interval_lemma_" << g_problem_id << ".smt2";
g_problem_id++; g_problem_id++;
return ous.str().c_str(); return ous.str();
} }
static void display_lemmas(unsynch_mpq_manager & nm, char const * result_term, static void display_lemmas(unsynch_mpq_manager & nm, char const * result_term,

4
src/test/no_overflow.cpp
View file

@ -529,8 +529,8 @@ void test_div(unsigned bvsize) {
Z3_del_context(ctx); Z3_del_context(ctx);
} }
typedef Z3_ast (Z3_API *NO_OVFL_ARITH_FUNC)(Z3_context ctx, Z3_ast t1, Z3_ast t2, bool is_signed); typedef Z3_ast (*NO_OVFL_ARITH_FUNC)(Z3_context ctx, Z3_ast t1, Z3_ast t2, bool is_signed);
typedef Z3_ast (Z3_API *ARITH_FUNC)(Z3_context ctx, Z3_ast t1, Z3_ast t2); typedef Z3_ast (*ARITH_FUNC)(Z3_context ctx, Z3_ast t1, Z3_ast t2);
typedef enum { OVFL_FUNC, UDFL_FUNC } overflow_type; typedef enum { OVFL_FUNC, UDFL_FUNC } overflow_type;

3
src/test/qe_arith.cpp
View file

@ -377,6 +377,9 @@ static void add_random_ineq(
case opt::t_mod: case opt::t_mod:
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
break; break;
default:
NOT_IMPLEMENTED_YET();
break;
} }
fmls.push_back(fml); fmls.push_back(fml);
mbo.add_constraint(vars, rational(coeff), rel); mbo.add_constraint(vars, rational(coeff), rel);