From 73cebc24c8de4511adac40549c074b68840205dd Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 8 Feb 2015 13:25:40 +0000
Subject: [PATCH] propagate_ineqs synchronization fix

---
 src/tactic/arith/bound_propagator.h         | 2 +-
 src/tactic/arith/linear_equation.h          | 2 +-
 src/tactic/arith/propagate_ineqs_tactic.cpp | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/tactic/arith/bound_propagator.h b/src/tactic/arith/bound_propagator.h
index 04f2e0e17..6ac405ebc 100644
--- a/src/tactic/arith/bound_propagator.h
+++ b/src/tactic/arith/bound_propagator.h
@@ -31,7 +31,7 @@ class bound_propagator {
 public:
     typedef unsigned var;
     typedef unsigned assumption;
-    typedef unsynch_mpq_manager numeral_manager;
+    typedef synch_mpq_manager numeral_manager;
     typedef unsigned_vector assumption_vector;
     typedef unsigned constraint_id;
     typedef numeral_buffer<mpz, numeral_manager> mpz_buffer;
diff --git a/src/tactic/arith/linear_equation.h b/src/tactic/arith/linear_equation.h
index 8b38a30e4..56349e2a4 100644
--- a/src/tactic/arith/linear_equation.h
+++ b/src/tactic/arith/linear_equation.h
@@ -52,7 +52,7 @@ public:
 
 class linear_equation_manager {
 public:
-    typedef unsynch_mpq_manager numeral_manager;
+    typedef synch_mpq_manager numeral_manager;
     typedef linear_equation::var var;
     typedef numeral_buffer<mpz, numeral_manager> mpz_buffer;
 private:
diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp
index 977f15167..6c284a0d4 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.cpp
+++ b/src/tactic/arith/propagate_ineqs_tactic.cpp
@@ -65,7 +65,7 @@ tactic * mk_propagate_ineqs_tactic(ast_manager & m, params_ref const & p) {
 
 struct propagate_ineqs_tactic::imp {
     ast_manager &          m;
-    unsynch_mpq_manager    nm;
+    synch_mpq_manager    nm;
     small_object_allocator m_allocator;
     bound_propagator       bp;
     arith_util             m_util;
@@ -73,7 +73,7 @@ struct propagate_ineqs_tactic::imp {
     obj_map<expr, a_var>   m_expr2var;
     expr_ref_vector        m_var2expr;
 
-    typedef numeral_buffer<mpq, unsynch_mpq_manager> mpq_buffer;
+    typedef numeral_buffer<mpq, synch_mpq_manager> mpq_buffer;
     typedef svector<a_var> var_buffer;                          
     
     mpq_buffer             m_num_buffer;