mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
deal with warning messages
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
5b8e3ae198
commit
cba9a160d3
|
@ -38,6 +38,7 @@ static void STD_CALL on_ctrl_c(int) {
|
|||
raise(SIGINT);
|
||||
}
|
||||
|
||||
#if 0
|
||||
static void display_model(sat::solver const & s) {
|
||||
sat::model const & m = s.get_model();
|
||||
for (unsigned i = 1; i < m.size(); i++) {
|
||||
|
@ -49,6 +50,7 @@ static void display_model(sat::solver const & s) {
|
|||
}
|
||||
std::cout << "\n";
|
||||
}
|
||||
#endif
|
||||
|
||||
static void display_status(lbool r) {
|
||||
switch (r) {
|
||||
|
|
|
@ -15,11 +15,12 @@ using namespace datalog;
|
|||
|
||||
|
||||
void tst_dl_context() {
|
||||
symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") };
|
||||
|
||||
return;
|
||||
|
||||
#if 0
|
||||
symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") };
|
||||
|
||||
const unsigned rel_cnt = sizeof(relations)/sizeof(symbol);
|
||||
const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog";
|
||||
|
||||
|
|
|
@ -89,6 +89,7 @@ private:
|
|||
expr_ref_vector& coefficients = poly.coefficients();
|
||||
expr_ref& coefficient = poly.coefficient();
|
||||
(void) coefficient;
|
||||
(void) coefficients;
|
||||
|
||||
m_rw(term);
|
||||
|
||||
|
@ -171,7 +172,7 @@ static expr_ref mk_mul(arith_util& arith, unsigned num_args, expr* const* args)
|
|||
|
||||
static void nf(expr_ref& term) {
|
||||
ast_manager& m = term.get_manager();
|
||||
expr *e1, *e2;
|
||||
expr *e1 = 0, *e2 = 0;
|
||||
|
||||
th_rewriter rw(m);
|
||||
arith_util arith(m);
|
||||
|
|
|
@ -34,11 +34,6 @@ static void add_clause(sat::solver& s, random_gen& r, trail_t& t) {
|
|||
s.mk_clause(cls.size(), cls.c_ptr());
|
||||
}
|
||||
|
||||
static void display_state(std::ostream& out, sat::solver& s, trail_t& t) {
|
||||
(void)t;
|
||||
s.display(out);
|
||||
}
|
||||
|
||||
static void pop_user_scope(sat::solver& s, trail_t& t) {
|
||||
std::cout << "pop\n";
|
||||
s.user_pop(1);
|
||||
|
|
|
@ -164,7 +164,7 @@ static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, m
|
|||
for (unsigned j = 0; j < roots.size(); j++) {
|
||||
if (to_rational(roots[j]) == r) {
|
||||
SASSERT(!visited[j]);
|
||||
SASSERT(!found);
|
||||
VERIFY(!found);
|
||||
found = true;
|
||||
visited[j] = true;
|
||||
}
|
||||
|
@ -172,7 +172,7 @@ static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, m
|
|||
for (unsigned j = 0; j < lowers.size(); j++) {
|
||||
unsigned j_prime = j + roots.size();
|
||||
if (to_rational(lowers[j]) < r && r < to_rational(uppers[j])) {
|
||||
SASSERT(!found);
|
||||
VERIFY(!found);
|
||||
SASSERT(!visited[j_prime]);
|
||||
found = true;
|
||||
visited[j_prime] = true;
|
||||
|
|
Loading…
Reference in a new issue