diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 034bb236a..4454e2fbf 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -1801,7 +1801,7 @@ namespace pdr {
             m_expanded_lvl = n.level();
         }
 
-        n.pt().set_use_farkas(m_params.use_farkas());
+        pred_transformer::scoped_farkas sf (n.pt(), m_params.use_farkas());
         if (n.pt().is_reachable(n.state())) {
             TRACE("pdr", tout << "reachable\n";);
             close_node(n);
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 4c26fc1ac..3501ca7cd 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -165,8 +165,19 @@ namespace pdr {
         void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars);
 
         prop_solver& get_solver() { return m_solver; }
+        prop_solver const& get_solver() const { return m_solver; }
 
         void set_use_farkas(bool f) { get_solver().set_use_farkas(f); }
+        bool get_use_farkas() const { return get_solver().get_use_farkas(); }
+        class scoped_farkas {
+            bool m_old;
+            pred_transformer& m_p;
+        public:
+            scoped_farkas(pred_transformer& p, bool v): m_old(p.get_use_farkas()), m_p(p) {
+                p.set_use_farkas(v);
+            }
+            ~scoped_farkas() { m_p.set_use_farkas(m_old); }
+        };
 
     };
 
diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp
index 5e928ff45..7321a1c03 100644
--- a/src/muz_qe/pdr_generalizers.cpp
+++ b/src/muz_qe/pdr_generalizers.cpp
@@ -196,7 +196,7 @@ namespace pdr {
 
                   );
             model_node nd(0, state, n.pt(), n.level());
-            n.pt().set_use_farkas(true);
+            pred_transformer::scoped_farkas sf(n.pt(), true);
             if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
                 TRACE("pdr", 
                       tout << mk_pp(state, m) << "\n";
@@ -261,7 +261,7 @@ namespace pdr {
             expr_ref state = pm.mk_and(conv1);
             TRACE("pdr", tout << "Try:\n" << mk_pp(state, m) << "\n";);
             model_node nd(0, state, n.pt(), n.level());
-            n.pt().set_use_farkas(true);
+            pred_transformer::scoped_farkas sf(n.pt(), true);
             if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
                 IF_VERBOSE(0,
                            verbose_stream() << mk_pp(state, m) << "\n";
diff --git a/src/muz_qe/pdr_prop_solver.h b/src/muz_qe/pdr_prop_solver.h
index 7712573ee..5a6b09360 100644
--- a/src/muz_qe/pdr_prop_solver.h
+++ b/src/muz_qe/pdr_prop_solver.h
@@ -99,6 +99,7 @@ namespace pdr {
         };
         
         void set_use_farkas(bool f) { m_use_farkas = f; }
+        bool get_use_farkas() const { return m_use_farkas; }
         
         void add_formula(expr * form);
         void add_level_formula(expr * form, unsigned level);