From d4d3ba104eae18e4815bb92fbf1081cbee75d186 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Mar 2013 21:41:00 -0700 Subject: [PATCH] fix compiler warning for unused variable Signed-off-by: Nikolaj Bjorner --- src/muz_qe/horn_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index b588b07ba..633aeaa81 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -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());