From 619bd91ddb30c6b6283409be567336ee390e692d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Jun 2013 11:59:40 -0500
Subject: [PATCH] fix bug in ctx-solver-simplify reported @
 http://z3.codeplex.com/workitem/51

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/tactic/ctx_solver_simplify_tactic.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
index 5668ca455..626cb6d22 100644
--- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp
+++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
@@ -218,7 +218,7 @@ protected:
                     else if (m.is_bool(arg)) {
                         res = local_simplify(a, n, id, i);
                         TRACE("ctx_solver_simplify_tactic", 
-                              tout << "Already cached: " << path_r.first << " " << mk_pp(res, m) << "\n";);
+                              tout << "Already cached: " << path_r.first << " " << mk_pp(arg, m) << " |-> " << mk_pp(res, m) << "\n";);
                         args.push_back(res);
                     }
                     else {
@@ -327,7 +327,7 @@ protected:
         tmp = m.mk_eq(result, n);
         m_solver.assert_expr(tmp);
         if (!simplify_bool(n2, result)) {
-            result = a;
+            result = a->get_arg(index);
         }
         m_solver.pop(1);
         return result;