From 4daecd5fb02016152a72b1e5b77f4548781372e0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Oct 2012 14:52:08 -0700 Subject: [PATCH] fixed compilation bug Signed-off-by: Leonardo de Moura --- src/tactic/ufbv_tactic/ufbv_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/ufbv_tactic/ufbv_tactic.cpp b/src/tactic/ufbv_tactic/ufbv_tactic.cpp index fa280c482..ac0bff8f0 100644 --- a/src/tactic/ufbv_tactic/ufbv_tactic.cpp +++ b/src/tactic/ufbv_tactic/ufbv_tactic.cpp @@ -19,7 +19,6 @@ Notes: #include"tactical.h" #include"simplify_tactic.h" #include"propagate_values_tactic.h" -#include"nnf.h" #include"solve_eqs_tactic.h" #include"simplifier.h" #include"basic_simplifier_plugin.h" @@ -35,6 +34,7 @@ Notes: #include"reduce_args_tactic.h" #include"smt_tactic.h" #include"ufbv_tactic.h" +#include"nnf_tactic.h" class macro_finder_tactic : public tactic {