diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index 3282fa2ba..2bf6fb7b0 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -5,6 +5,8 @@ Version 4.3.2
 
 - Added get_version() and get_version_string() to Z3Py
 
+- Added support for FreeBSD. Z3 can be compiled on FreeBSD using g++. 
+
 Version 4.3.1
 =============
 
diff --git a/configure.ac b/configure.ac
index a02915ff4..a2e2d826d 100644
--- a/configure.ac
+++ b/configure.ac
@@ -101,15 +101,15 @@ AC_PROG_SED
 
 AS_IF([test "$CXX" = "g++"], [
    # Enable OpenMP
-   CXXFLAGS+=" -fopenmp"  
-   LDFLAGS+=" -fopenmp"
-   SLIBEXTRAFLAGS+=" -fopenmp"
+   CXXFLAGS="$CXXFLAGS -fopenmp"  
+   LDFLAGS="$LDFLAGS -fopenmp"
+   SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -fopenmp"
    # Use -mfpmath=sse
-   CXXFLAGS+=" -mfpmath=sse"
+   CXXFLAGS="$CXXFLAGS -mfpmath=sse"
 ],
       [test "$CXX" = "clang++"], [
    # OpenMP is not supported in clang++
-   CXXFLAGS+=" -D _NO_OMP_"  
+   CXXFLAGS="$CXXFLAGS -D _NO_OMP_"  
 ],
 [
   AC_MSG_ERROR([Unsupported compiler: $CXX])
@@ -128,28 +128,38 @@ host_os=`uname -s`
 AS_IF([test "$host_os" = "Darwin"], [
   PLATFORM=osx
   SO_EXT=.dylib
-  SLIBFLAGS+="-dynamiclib"
+  SLIBFLAGS="$SLIBFLAGS -dynamiclib"
   COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)"
   STATIC_FLAGS=
 ], [test "$host_os" = "Linux"], [
+  CXXFLAGS=$CXXFLAGS -D _LINUX_
   PLATFORM=linux
   SO_EXT=.so
-  LDFLAGS+=" -lrt"
-  SLIBFLAGS+=" -shared"
+  LDFLAGS="$LDFLAGS -lrt"
+  SLIBFLAGS="$SLIBFLAGS -shared"
   COMP_VERSIONS=
   STATIC_FLAGS=-static
-  CXXFLAGS+=" -fno-strict-aliasing"
+  CXXFLAGS="$CXXFLAGS -fno-strict-aliasing"
   if test "$CXX" = "clang++"; then
      # More flags for clang++ for Linux
-     CXXFLAGS+=" -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value"
+     CXXFLAGS="$CXXFLAGS -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value"
   fi
-  SLIBEXTRAFLAGS+=" -lrt"
+  SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -lrt"
+], [test "$host_os" = "FreeBSD"], [
+   CXXFLAGS="$CXXFLAGS -D _FREEBSD_"
+   PLATFORM=bsd
+   SO_EXT=.so
+   LDFLAGS="$LDFLAGS -lrt"
+   SLIBFLAGS="$SLIBFLAGS -shared"
+   COMP_VERSIONS=
+   STATIC_FLAGS=-static
+   SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -lrt"
 ], [test "${host_os:0:6}" = "CYGWIN"], [
    PLATFORM=win
    SO_EXT=.dll
-   SLIBFLAGS+="-shared"
+   SLIBFLAGS="$SLIBFLAGS -shared"
    COMP_VERSIONS=
-   CXXFLAGS+=" -D_CYGWIN -fno-strict-aliasing"
+   CXXFLAGS="$CXXFLAGS -D_CYGWIN -fno-strict-aliasing"
 ],
 [
   AC_MSG_ERROR([Unknown host platform: $host_os])
@@ -169,11 +179,11 @@ AC_CHECK_SIZEOF(int *)
 
 if test $ac_cv_sizeof_int_p -eq 8; then
    dnl In 64-bit systems we have to compile using -fPIC
-   CXXFLAGS+=" -fPIC"
-   CPPFLAGS+=" -D_AMD64_"
+   CXXFLAGS="$CXXFLAGS -fPIC"
+   CPPFLAGS="$CPPFLAGS -D_AMD64_"
    dnl Only enable use of thread local storage for 64-bit Linux. It is disabled for OSX and 32-bit Linux
    if test $PLATFORM = "linux"; then
-      CPPFLAGS+=" -D_USE_THREAD_LOCAL" 
+      CPPFLAGS="$CPPFLAGS -D_USE_THREAD_LOCAL" 
    fi
    IS_X64="yes"
 else
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index 944eb1e26..713727f05 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -29,6 +29,7 @@ Revision History:
 #include"vector.h"
 #include"for_each_ast.h"
 #include"decl_collector.h"
+#include"smt2_util.h"
 
 // ---------------------------------------
 // smt_renaming
@@ -67,32 +68,10 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {
         return symbol(buffer.str().c_str());            
     }
     
-    buffer << "|";
-    if (*data == '|') {
-        while (*data) {
-            if (*data == '|') {
-                if (!data[1]) {
-                    break;
-                }
-                buffer << "\\";
-            }
-            buffer << *data;
-            ++data;
-        }                      
-    }
-    else {
-        while (*data) {
-            if (*data == '|') {
-                buffer << "\\";
-            }
-            buffer << *data;
-            ++data;
-        }
-    }
+    buffer << mk_smt2_quoted_symbol(s);
     if (k > 0) {
         buffer << k;
     }
-    buffer << "|";
     
     return symbol(buffer.str().c_str());
 }
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index ecd9ee5cb..13008d059 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -1683,7 +1683,8 @@ namespace datalog {
         for (unsigned i = 0; i < rules.size(); ++i) {            
             out << (use_fixedpoint_extensions?"(rule ":"(assert ");
             expr* r = rules[i].get();
-            if (symbol::null != names[i]) {
+            symbol nm = names[i];
+            if (symbol::null != nm) {
                 out << "(! ";
             }
             if (use_fixedpoint_extensions) {
@@ -1692,8 +1693,14 @@ namespace datalog {
             else {
                 out << mk_smt_pp(r, m);
             }
-            if (symbol::null != names[i]) {
-                out << " :named " << names[i] << ")";
+            if (symbol::null != nm) {
+                while (fresh_names.contains(nm)) {
+                    std::ostringstream s;
+                    s << nm << "!";
+                    nm = symbol(s.str().c_str());                    
+                }
+                fresh_names.add(nm);
+                out << " :named " << nm << ")";
             }
             out << ")\n";
         }
diff --git a/src/muz_qe/pdr_tactic.cpp b/src/muz_qe/horn_tactic.cpp
similarity index 93%
rename from src/muz_qe/pdr_tactic.cpp
rename to src/muz_qe/horn_tactic.cpp
index 6b1b13e67..1e76faf13 100644
--- a/src/muz_qe/pdr_tactic.cpp
+++ b/src/muz_qe/horn_tactic.cpp
@@ -3,11 +3,11 @@ Copyright (c) 2012 Microsoft Corporation
 
 Module Name:
 
-    pdr_tactic.h
+    horn_tactic.h
 
 Abstract:
 
-    PDR as a tactic to solve Horn clauses.
+    HORN as a tactic to solve Horn clauses.
 
 Author:
 
@@ -19,10 +19,10 @@ Revision History:
 #include"tactical.h"
 #include"model_converter.h"
 #include"proof_converter.h"
-#include"pdr_tactic.h"
+#include"horn_tactic.h"
 #include"dl_context.h"
 
-class pdr_tactic : public tactic {
+class horn_tactic : public tactic {
     struct imp {
         ast_manager&             m;
         datalog::context         m_ctx;
@@ -139,7 +139,7 @@ class pdr_tactic : public tactic {
                         expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
             mc = 0; pc = 0; core = 0;
-            tactic_report report("pdr", *g);
+            tactic_report report("horn", *g);
             bool produce_models = g->models_enabled();
             bool produce_proofs = g->proofs_enabled();
 
@@ -174,6 +174,7 @@ class pdr_tactic : public tactic {
 
             if (queries.size() != 1) {
                 q = m.mk_fresh_const("query", m.mk_bool_sort());
+                register_predicate(q);
                 for (unsigned i = 0; i < queries.size(); ++i) {
                     f = mk_rule(queries[i].get(), q);
                     m_ctx.add_rule(f, symbol::null);
@@ -209,7 +210,7 @@ class pdr_tactic : public tactic {
                 // subgoal is unchanged.
                 break;    
             }
-            TRACE("pdr", g->display(tout););
+            TRACE("horn", g->display(tout););
             SASSERT(g->is_well_sorted());
         }
     };
@@ -217,16 +218,16 @@ class pdr_tactic : public tactic {
     params_ref m_params;
     imp *      m_imp;
 public:
-    pdr_tactic(ast_manager & m, params_ref const & p):
+    horn_tactic(ast_manager & m, params_ref const & p):
         m_params(p) {
         m_imp = alloc(imp, m, p);
     }
 
     virtual tactic * translate(ast_manager & m) {
-        return alloc(pdr_tactic, m, m_params);
+        return alloc(horn_tactic, m, m_params);
     }
         
-    virtual ~pdr_tactic() {
+    virtual ~horn_tactic() {
         dealloc(m_imp);
     }
 
@@ -280,7 +281,7 @@ protected:
     }
 };
 
-tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p) {
-    return clean(alloc(pdr_tactic, m, p));
+tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(horn_tactic, m, p));
 }
 
diff --git a/src/muz_qe/pdr_tactic.h b/src/muz_qe/horn_tactic.h
similarity index 53%
rename from src/muz_qe/pdr_tactic.h
rename to src/muz_qe/horn_tactic.h
index 5a315152a..7f56a77ba 100644
--- a/src/muz_qe/pdr_tactic.h
+++ b/src/muz_qe/horn_tactic.h
@@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation
 
 Module Name:
 
-    pdr_tactic.h
+    horn_tactic.h
 
 Abstract:
 
@@ -16,15 +16,15 @@ Author:
 Revision History:
 
 --*/
-#ifndef _PDR_TACTIC_H_
-#define _PDR_TACTIC_H_
+#ifndef _HORN_TACTIC_H_
+#define _HORN_TACTIC_H_
 
 #include"params.h"
 class ast_manager;
 class tactic;
 
-tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p = params_ref());
+tactic * mk_horn_tactic(ast_manager & m, params_ref const & p = params_ref());
 /*
-  ADD_TACTIC("pdr", "apply pdr for horn clauses.", "mk_pdr_tactic(m, p)")
+  ADD_TACTIC("horn", "apply tactic for horn clauses.", "mk_horn_tactic(m, p)")
 */
 #endif
diff --git a/src/muz_qe/model2expr.h b/src/muz_qe/model2expr.h
index 9a63d6b8c..3fd2e4524 100644
--- a/src/muz_qe/model2expr.h
+++ b/src/muz_qe/model2expr.h
@@ -35,7 +35,9 @@ class mk_fresh_name {
 public:
     mk_fresh_name(): m_char('A'), m_num(0) {}
     void add(ast* a);
+    void add(symbol const& s) { m_symbols.insert(s); }
     symbol next();
+    bool contains(symbol const& s) const { return m_symbols.contains(s); }
 };
 
 
diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp
index 574be63b1..d70675d80 100644
--- a/src/muz_qe/pdr_prop_solver.cpp
+++ b/src/muz_qe/pdr_prop_solver.cpp
@@ -26,6 +26,7 @@ Revision History:
 #include "model_pp.h"
 #include "front_end_params.h"
 #include "datatype_decl_plugin.h"
+#include "bv_decl_plugin.h"
 #include "pdr_farkas_learner.h"
 #include "ast_smt2_pp.h"
 #include "expr_replacer.h"
@@ -94,9 +95,12 @@ namespace pdr {
         void expand_literals(expr_ref_vector& conjs) {
             arith_util arith(m);
             datatype_util dt(m);
+            bv_util       bv(m);
             expr* e1, *e2, *c, *val;
-            for (unsigned i = 0; i < conjs.size(); ++i) {
+            rational r;
+            unsigned bv_size;
 
+            for (unsigned i = 0; i < conjs.size(); ++i) {
                 expr* e = conjs[i].get();
                 if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) {
                     conjs[i] = arith.mk_le(e1,e2);
@@ -109,7 +113,8 @@ namespace pdr {
                     }
                     ++i;
                 }
-                else if (m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) {
+                else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) ||
+                         (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){
                     func_decl* f = to_app(val)->get_decl();
                     func_decl* r = dt.get_constructor_recognizer(f);
                     conjs[i] = m.mk_app(r,c);
@@ -118,6 +123,24 @@ namespace pdr {
                         conjs.push_back(m.mk_eq(m.mk_app(acc[i], c), to_app(val)->get_arg(i)));
                     }
                 }
+                else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) ||
+                         (m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) {
+                    rational two(2);
+                    for (unsigned j = 0; j < bv_size; ++j) {
+                        parameter p(j);
+                        expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c);
+                        if ((r % two).is_zero()) {
+                            e = m.mk_not(e);
+                        }
+                        r = div(r, two);
+                        if (j == 0) {
+                            conjs[i] = e;
+                        }
+                        else {
+                            conjs.push_back(e);
+                        }
+                    }
+                }
             }
         }
 
@@ -341,7 +364,7 @@ namespace pdr {
         }
         fl.get_lemmas(pr, bs, lemmas);
         safe.elim_proxies(lemmas);
-        fl.simplify_lemmas(lemmas); // redundant
+        fl.simplify_lemmas(lemmas); // redundant?
         if (m_fparams.m_arith_mode == AS_DIFF_LOGIC &&
             !is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) {
                 IF_VERBOSE(1, 
diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp
index ec042e33d..97f55fb6f 100644
--- a/src/muz_qe/qe_lite.cpp
+++ b/src/muz_qe/qe_lite.cpp
@@ -342,17 +342,22 @@ class der2 {
 
     void apply_substitution(quantifier * q, expr_ref & r) {
         expr * e = q->get_expr();
-        unsigned num_args = to_app(e)->get_num_args(); 
+        unsigned num_args = 1;
+        expr* const* args = &e;
+        if ((q->is_forall() && m.is_or(e)) ||
+            (q->is_exists() && m.is_and(e))) {
+            num_args = to_app(e)->get_num_args();
+            args     = to_app(e)->get_args();
+        }
         bool_rewriter rw(m);
         
         // get a new expression
         m_new_args.reset();
         for(unsigned i = 0; i < num_args; i++) {
             int x = m_pos2var[i];
-            if (x != -1 && m_map[x] != 0) 
-                continue; // this is a disequality/equality with definition (vanishes)
-            
-            m_new_args.push_back(to_app(e)->get_arg(i));
+            if (x == -1 || m_map[x] == 0) {
+                m_new_args.push_back(args[i]);
+            }
         }
         
         expr_ref t(m);
diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h
index 09a1a4de2..291120e92 100644
--- a/src/tactic/fpa/fpa2bv_converter.h
+++ b/src/tactic/fpa/fpa2bv_converter.h
@@ -197,4 +197,4 @@ protected:
     void convert(model * bv_mdl, model * float_mdl);
 };
 
-#endif
\ No newline at end of file
+#endif
diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h
new file mode 100644
index 000000000..62c6f1a2d
--- /dev/null
+++ b/src/tactic/fpa/fpa2bv_rewriter.h
@@ -0,0 +1,166 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    fpa2bv_rewriter.h
+
+Abstract:
+
+    Rewriter for converting FPA to BV
+
+Author:
+
+    Christoph (cwinter) 2012-02-09
+
+Notes:
+
+--*/
+
+#ifndef _FPA2BV_REWRITER_H_
+#define _FPA2BV_REWRITER_H_
+
+#include"cooperate.h"
+#include"rewriter_def.h"
+#include"bv_decl_plugin.h"
+#include"fpa2bv_converter.h"
+
+struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
+    ast_manager              & m_manager;    
+    expr_ref_vector            m_out;    
+    fpa2bv_converter         & m_conv;
+
+    unsigned long long         m_max_memory;
+    unsigned                   m_max_steps;
+
+    ast_manager & m() const { return m_manager; }
+
+    fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
+        m_manager(m),
+        m_out(m),
+        m_conv(c) {
+        updt_params(p);
+        // We need to make sure that the mananger has the BV plugin loaded.
+        symbol s_bv("bv");
+        if (!m_manager.has_plugin(s_bv))
+            m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
+    }
+
+    ~fpa2bv_rewriter_cfg() {        
+    }
+
+    void cleanup_buffers() {
+        m_out.finalize();
+    }
+
+    void updt_params(params_ref const & p) {
+        m_max_memory     = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+        m_max_steps      = p.get_uint(":max-steps", UINT_MAX);        
+    }
+
+    bool max_steps_exceeded(unsigned num_steps) const { 
+        cooperate("fpa2bv");
+        if (memory::get_allocation_size() > m_max_memory)
+            throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+        return num_steps > m_max_steps;
+    }
+
+    br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+        TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
+
+        if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
+            m_conv.mk_const(f, result);
+            return BR_DONE;
+        }
+
+		if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm_sort(f->get_range())) {
+            m_conv.mk_rm_const(f, result);
+            return BR_DONE;
+        }
+
+        if (m().is_eq(f)) {
+            SASSERT(num == 2);
+            if (m_conv.is_float(args[0])) {
+                m_conv.mk_eq(args[0], args[1], result);
+                return BR_DONE;
+            }
+            return BR_FAILED;
+        }
+
+        if (m().is_ite(f)) {
+            SASSERT(num == 3);
+            if (m_conv.is_float(args[1])) {
+                m_conv.mk_ite(args[0], args[1], args[2], result);
+                return BR_DONE;
+            }
+            return BR_FAILED;
+        }
+        
+        if (m_conv.is_float_family(f)) {
+            switch (f->get_decl_kind()) {            
+            case OP_RM_NEAREST_TIES_TO_AWAY:
+            case OP_RM_NEAREST_TIES_TO_EVEN:
+            case OP_RM_TOWARD_NEGATIVE:
+            case OP_RM_TOWARD_POSITIVE:
+			case OP_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE;            
+            case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE;                             
+            case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE;
+            case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE;
+            case OP_FLOAT_NAN: m_conv.mk_nan(f, result); return BR_DONE;
+            case OP_FLOAT_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_UMINUS: m_conv.mk_uminus(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_REM: m_conv.mk_remainder(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_FUSED_MA: m_conv.mk_fusedma(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
+            case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
+            default:
+                TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
+                      for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
+                throw tactic_exception("NYI");
+            }
+        }
+        
+        return BR_FAILED;
+    }
+
+    bool reduce_quantifier(quantifier * old_q, 
+                           expr * new_body, 
+                           expr * const * new_patterns, 
+                           expr * const * new_no_patterns,
+                           expr_ref & result,
+                           proof_ref & result_pr) {
+        return false;
+    }
+
+    bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { 
+        return false; 
+    }
+};
+
+template class rewriter_tpl<fpa2bv_rewriter_cfg>;
+
+struct fpa2bv_rewriter : public rewriter_tpl<fpa2bv_rewriter_cfg> {
+    fpa2bv_rewriter_cfg m_cfg;
+    fpa2bv_rewriter(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
+        rewriter_tpl<fpa2bv_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),        
+        m_cfg(m, c, p) {
+    }
+};
+
+#endif
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index a4e46472a..79f41518e 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -17,156 +17,10 @@ Notes:
 
 --*/
 #include"tactical.h"
-#include"rewriter_def.h"
-#include"cooperate.h"
-#include"ref_util.h"
-#include"bv_decl_plugin.h"
-#include"float_decl_plugin.h"
-#include"fpa2bv_converter.h"
-
-#include"tactical.h"
+#include"fpa2bv_rewriter.h"
 #include"simplify_tactic.h"
-
 #include"fpa2bv_tactic.h"
 
-struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
-    ast_manager              & m_manager;    
-    expr_ref_vector            m_out;    
-    fpa2bv_converter         & m_conv;
-
-    unsigned long long         m_max_memory;
-    unsigned                   m_max_steps;
-
-    ast_manager & m() const { return m_manager; }
-
-    fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
-        m_manager(m),
-        m_out(m),
-        m_conv(c) {
-        updt_params(p);
-        // We need to make sure that the mananger has the BV plugin loaded.
-        symbol s_bv("bv");
-        if (!m_manager.has_plugin(s_bv))
-            m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
-    }
-
-    ~fpa2bv_rewriter_cfg() {        
-    }
-
-    void cleanup_buffers() {
-        m_out.finalize();
-    }
-
-    void updt_params(params_ref const & p) {
-        m_max_memory     = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
-        m_max_steps      = p.get_uint(":max-steps", UINT_MAX);        
-    }
-
-    bool max_steps_exceeded(unsigned num_steps) const { 
-        cooperate("fpa2bv");
-        if (memory::get_allocation_size() > m_max_memory)
-            throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
-        return num_steps > m_max_steps;
-    }
-
-    br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
-        TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
-
-        if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
-            m_conv.mk_const(f, result);
-            return BR_DONE;
-        }
-
-		if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm_sort(f->get_range())) {
-            m_conv.mk_rm_const(f, result);
-            return BR_DONE;
-        }
-
-        if (m().is_eq(f)) {
-            SASSERT(num == 2);
-            if (m_conv.is_float(args[0])) {
-                m_conv.mk_eq(args[0], args[1], result);
-                return BR_DONE;
-            }
-            return BR_FAILED;
-        }
-
-        if (m().is_ite(f)) {
-            SASSERT(num == 3);
-            if (m_conv.is_float(args[1])) {
-                m_conv.mk_ite(args[0], args[1], args[2], result);
-                return BR_DONE;
-            }
-            return BR_FAILED;
-        }
-        
-        if (m_conv.is_float_family(f)) {
-            switch (f->get_decl_kind()) {            
-            case OP_RM_NEAREST_TIES_TO_AWAY:
-            case OP_RM_NEAREST_TIES_TO_EVEN:
-            case OP_RM_TOWARD_NEGATIVE:
-            case OP_RM_TOWARD_POSITIVE:
-			case OP_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE;            
-            case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE;                             
-            case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE;
-            case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE;
-            case OP_FLOAT_NAN: m_conv.mk_nan(f, result); return BR_DONE;
-            case OP_FLOAT_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_UMINUS: m_conv.mk_uminus(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_REM: m_conv.mk_remainder(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_FUSED_MA: m_conv.mk_fusedma(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
-            case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
-            default:
-                TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
-                      for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
-                throw tactic_exception("NYI");
-            }
-        }
-        
-        return BR_FAILED;
-    }
-
-    bool reduce_quantifier(quantifier * old_q, 
-                           expr * new_body, 
-                           expr * const * new_patterns, 
-                           expr * const * new_no_patterns,
-                           expr_ref & result,
-                           proof_ref & result_pr) {
-        return false;
-    }
-
-    bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { 
-        return false; 
-    }
-};
-
-template class rewriter_tpl<fpa2bv_rewriter_cfg>;
-
-struct fpa2bv_rewriter : public rewriter_tpl<fpa2bv_rewriter_cfg> {
-    fpa2bv_rewriter_cfg m_cfg;
-    fpa2bv_rewriter(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
-        rewriter_tpl<fpa2bv_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),        
-        m_cfg(m, c, p) {
-    }
-};
-
 class fpa2bv_tactic : public tactic {
     struct imp {
         ast_manager &     m;
diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp
index dd656666c..d034000c4 100644
--- a/src/tactic/fpa/qffpa_tactic.cpp
+++ b/src/tactic/fpa/qffpa_tactic.cpp
@@ -35,4 +35,4 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) {
                     using_params(mk_simplify_tactic(m, p), sat_simp_p),
                     mk_sat_tactic(m, p),
                     mk_fail_if_undecided_tactic());
-}
\ No newline at end of file
+}
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index eb0534eea..4cf530b1e 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -33,7 +33,7 @@ Notes:
 #include"default_tactic.h"
 #include"ufbv_tactic.h"
 #include"qffpa_tactic.h"
-#include"pdr_tactic.h"
+#include"horn_tactic.h"
 #include"smt_solver.h"
 
 MK_SIMPLE_TACTIC_FACTORY(qfuf_fct, mk_qfuf_tactic(m, p));
@@ -55,7 +55,7 @@ MK_SIMPLE_TACTIC_FACTORY(qfnia_fct, mk_qfnia_tactic(m, p));
 MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p));
 MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p));
 MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p));
-MK_SIMPLE_TACTIC_FACTORY(horn_fct, mk_pdr_tactic(m, p));
+MK_SIMPLE_TACTIC_FACTORY(horn_fct, mk_horn_tactic(m, p));
 
 static void init(strategic_solver * s) {
     s->set_default_tactic(alloc(default_fct));
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index bde735a69..5f9d554f9 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -33,15 +33,22 @@ Revision History:
 #include<sys/time.h>
 #include<sys/errno.h>
 #include<pthread.h>
-#else
+#elif defined(_LINUX_) || defined(_FREEBSD_)
 // Linux
 #include<csignal>
 #include<ctime>
 #include<memory.h>
 #include"warning.h"
-#define CLOCKID CLOCK_PROCESS_CPUTIME_ID
+   #ifdef _LINUX_
+   #define CLOCKID CLOCK_PROCESS_CPUTIME_ID
+   #else
+   // FreeBSD does not support CLOCK_PROCESS_CPUTIME_ID 
+   #define CLOCKID CLOCK_PROF
+   #endif
 #define SIG     SIGRTMIN
 // ---------
+#else
+// Other platforms
 #endif 
 
 #include"scoped_timer.h"
@@ -63,12 +70,14 @@ struct scoped_timer::imp {
     pthread_attr_t   m_attributes;
     unsigned         m_interval;    
     pthread_cond_t   m_condition_var;
-#else
-    // Linux
+#elif defined(_LINUX_) || defined(_FREEBSD_)
+    // Linux & FreeBSD
     static void *   g_timer;
     void            (*m_old_handler)(int);
     void *          m_old_timer;
     timer_t         m_timerid;
+#else
+    // Other
 #endif
 
 #if defined(_WINDOWS) || defined(_CYGWIN)
@@ -117,10 +126,12 @@ struct scoped_timer::imp {
             throw default_exception("failed to destroy pthread condition variable");
         return st;
     }
-#else
+#elif defined(_LINUX_) || defined(_FREEBSD_)
     static void sig_handler(int) {
        static_cast<imp*>(g_timer)->m_eh->operator()();
     }
+#else
+    // Other
 #endif
 
 
@@ -142,8 +153,8 @@ struct scoped_timer::imp {
             throw default_exception("failed to initialize timer thread attributes");
         if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0)
             throw default_exception("failed to start timer thread");
-#else
-	// Linux version
+#elif defined(_LINUX_) || defined(_FREEBSD_)
+	// Linux & FreeBSD
         if (omp_in_parallel()) {
             // It doesn't work in with more than one thread.
             // SIGEV_SIGNAL: the event is handled by the process not by the thread that installed the handler.
@@ -172,6 +183,8 @@ struct scoped_timer::imp {
 	its.it_interval.tv_nsec = 0;
 	if (timer_settime(m_timerid, 0, &its, NULL) == -1)
 	    throw default_exception("failed to set timer");
+#else
+	// Other platforms
 #endif
     }
 
@@ -187,14 +200,16 @@ struct scoped_timer::imp {
             throw default_exception("failed to join thread");
         if (pthread_attr_destroy(&m_attributes) != 0)
             throw default_exception("failed to destroy pthread attributes object");
-#else
-	// Linux version
+#elif defined(_LINUX_) || defined(_FREEBSD_)
+	// Linux & FreeBSD
         if (omp_in_parallel())
             return; // see comments in the constructor.
 	timer_delete(m_timerid);
 	if (m_old_handler != SIG_ERR)
 	    signal(SIG, m_old_handler);
 	g_timer = m_old_timer;
+#else
+	// Other Platforms
 #endif
     }
 
@@ -203,9 +218,11 @@ struct scoped_timer::imp {
 #if defined(_WINDOWS) || defined(_CYGWIN)
 #elif defined(__APPLE__) && defined(__MACH__)
 // Mac OS X
-#else
-// Linux
+#elif defined(_LINUX_) || defined(_FREEBSD_)
+// Linux & FreeBSD
 void * scoped_timer::imp::g_timer = 0;
+#else
+// Other platforms
 #endif
 
 scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {