mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

fix compiler warning for unused variable

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-03-18 21:41:00 -07:00
parent d1ffeb36b0
commit d4d3ba104e
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/horn_tactic.cpp
View file

@ -169,7 +169,6 @@ class horn_tactic : public tactic {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
tactic_report report("horn", *g);
bool produce_models = g->models_enabled();
bool produce_proofs = g->proofs_enabled();
if (produce_proofs) {
@ -233,6 +232,7 @@ class horn_tactic : public tactic {
lbool is_reachable = m_ctx.query(q);
g->inc_depth();
bool produce_models = g->models_enabled();
bool produce_proofs = g->proofs_enabled();
result.push_back(g.get());