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

fix warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-23 12:14:34 -06:00
parent 6321dabe93
commit 794aafa6f8
4 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/cmd_context/extra_cmds/dbg_cmds.cpp
View file

@ -398,7 +398,7 @@ public:
ast_manager& m = ctx.m();
qe::interpolator mbi(m);
expr_ref itp(m);
lbool res = mbi.pogo(ctx.get_solver_factory(), m_a, m_b, itp);
mbi.pogo(ctx.get_solver_factory(), m_a, m_b, itp);
ctx.regular_stream() << itp << "\n";
}
};

3
src/qe/qe_term_graph.cpp
View file

@ -1267,11 +1267,12 @@ namespace qe {
for (auto const& terms : partitions) {
expr* a = nullptr;
for (expr* b : terms) {
if (is_uninterp(b))
if (is_uninterp(b)) {
if (a)
result.push_back(m.mk_eq(a, b));
else
a = b;
}
}
}
TRACE("qe", tout << result << "\n";);

2
src/sat/sat_aig_simplifier.cpp
View file

@ -426,7 +426,7 @@ namespace sat {
// Assign higher cutset budgets to equality candidates that come from simulation
// touch them to trigger recomputation of cutsets.
u64_map<literal> val2lit;
unsigned i = 0, j = 0, num_eqs = 0;
unsigned i = 0, num_eqs = 0;
for (cut_val val : var2val) {
if (!s.was_eliminated(i) && s.value(i) == l_undef) {
literal u(i, false), v;

1
src/smt/theory_fpa.cpp
View file

@ -724,7 +724,6 @@ namespace smt {
void theory_fpa::init_model(model_generator & mg) {
TRACE("t_fpa", tout << "initializing model" << std::endl; display(tout););
ast_manager & m = get_manager();
context & ctx = get_context();
m_factory = alloc(fpa_value_factory, m, get_family_id());
mg.register_factory(m_factory);
}