mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

misc warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-31 13:01:02 -07:00
parent ada873631e
commit b723e1093b
4 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/muz/spacer/spacer_manager.cpp
View file

@ -247,7 +247,7 @@ bool is_zk_const (const app *a, int &n) {
} }
bool sk_lt_proc::operator()(const app *a1, const app *a2) { bool sk_lt_proc::operator()(const app *a1, const app *a2) {
if (a1 == a2) return false; if (a1 == a2) return false;
int n1, n2; int n1 = 0, n2 = 0;
bool z1, z2; bool z1, z2;
z1 = is_zk_const(a1, n1); z1 = is_zk_const(a1, n1);
z2 = is_zk_const(a2, n2); z2 = is_zk_const(a2, n2);

1
src/sat/smt/euf_model.cpp
View file

@ -284,6 +284,7 @@ namespace euf {
tout << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n"; tout << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
s().display(tout); s().display(tout);
tout << mdl << "\n";); tout << mdl << "\n";);
(void)first;
first = false; first = false;
} }

1
src/sat/smt/fpa_solver.cpp
View file

@ -121,7 +121,6 @@ namespace fpa {
bool solver::post_visit(expr* e, bool sign, bool root) { bool solver::post_visit(expr* e, bool sign, bool root) {
euf::enode* n = expr2enode(e); euf::enode* n = expr2enode(e);
app* a = to_app(e);
SASSERT(!n || !n->is_attached_to(get_id())); SASSERT(!n || !n->is_attached_to(get_id()));
if (!n) if (!n)
n = mk_enode(e, false); n = mk_enode(e, false);

12
src/smt/theory_str.cpp
View file

@ -1859,18 +1859,18 @@ namespace smt {
axiomatized_terms.insert(ex); axiomatized_terms.insert(ex);
TRACE("str", tout << "instantiate str.from_code axiom for " << mk_pp(ex, m) << std::endl;); TRACE("str", tout << "instantiate str.from_code axiom for " << mk_pp(ex, m) << std::endl;);
expr * arg; expr * arg = nullptr;
u.str.is_from_code(ex, arg); VERIFY(u.str.is_from_code(ex, arg));
// (str.from_code N) == "" if N is not in the range [0, max_char]. // (str.from_code N) == "" if N is not in the range [0, max_char].
{ {
expr_ref premise(m.mk_or(m_autil.mk_le(arg, mk_int(-1)), m_autil.mk_ge(arg, mk_int(u.max_char() + 1))), m); expr_ref premise(m.mk_or(m_autil.mk_le(arg, mk_int(-1)), m_autil.mk_ge(arg, mk_int(u.max_char() + 1))), m);
expr_ref conclusion(ctx.mk_eq_atom(ex, mk_string("")), m); expr_ref conclusion(ctx.mk_eq_atom(ex, mk_string("")), m);
expr_ref axiom(rewrite_implication(premise, conclusion), m); expr_ref axiom(rewrite_implication(premise, conclusion), m);
assert_axiom_rw(axiom); assert_axiom_rw(axiom);
} }
// len (str.from_code N) == 1 if N is in the range [0, max_char]. // len (str.from_code N) == 1 if N is in the range [0, max_char].
{ {
expr_ref premise(m.mk_and(m_autil.mk_ge(arg, mk_int(0)), m_autil.mk_le(arg, mk_int(u.max_char() + 1))), m); expr_ref premise(m.mk_and(m_autil.mk_ge(arg, mk_int(0)), m_autil.mk_le(arg, mk_int(u.max_char() + 1))), m);
expr_ref conclusion(ctx.mk_eq_atom(mk_strlen(ex), mk_int(1)), m); expr_ref conclusion(ctx.mk_eq_atom(mk_strlen(ex), mk_int(1)), m);
expr_ref axiom(rewrite_implication(premise, conclusion), m); expr_ref axiom(rewrite_implication(premise, conclusion), m);
assert_axiom_rw(axiom); assert_axiom_rw(axiom);
@ -1895,8 +1895,8 @@ namespace smt {
axiomatized_terms.insert(ex); axiomatized_terms.insert(ex);
TRACE("str", tout << "instantiate str.to_code axiom for " << mk_pp(ex, m) << std::endl;); TRACE("str", tout << "instantiate str.to_code axiom for " << mk_pp(ex, m) << std::endl;);
expr * arg; expr * arg = nullptr;
u.str.is_to_code(ex, arg); VERIFY(u.str.is_to_code(ex, arg));
// (str.to_code S) == -1 if len(S) != 1. // (str.to_code S) == -1 if len(S) != 1.
{ {
expr_ref premise(m.mk_not(ctx.mk_eq_atom(mk_strlen(arg), mk_int(1))), m); expr_ref premise(m.mk_not(ctx.mk_eq_atom(mk_strlen(arg), mk_int(1))), m);