From b197e590a4a9d816be3dbb2f72ddc4308056e3eb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Oct 2015 19:25:38 -0700
Subject: [PATCH] fix coercion regression. Issue #263

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith_aux.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 8713c4fdb..0622f03ff 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1602,6 +1602,7 @@ namespace smt {
 
             TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n";
                   tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";);
+
             
             if (!has_bound && x_i == null_theory_var && x_j == null_theory_var) {
                 has_shared = false;