From d86c2889288b04661a65ee42009667a438e983ed Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Tue, 11 Aug 2015 09:22:09 -0700
Subject: [PATCH] More logging

---
 src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs b/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs
index cbe589eb..360aedff 100644
--- a/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs
+++ b/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs
@@ -450,12 +450,14 @@ cryCheckLinRel s logger x y p1 p2 =
                   | a <  0     = K (Nat b) :- K (Nat (negate a)) :* Var x
                   | otherwise  = sumTerm (K (Nat a) :* Var x)
 
+            SMT.logMessage logger ("candidate: " ++ show (ppProp (Var y :==: expr)))
+
             proved <- checkUnsat s
                     $ propToSmtLib $ crySimplify
                     $ Not $ Var y :==: expr
 
             if not proved
-               then return Nothing
+               then SMT.logMessage logger "failed" >> return Nothing
                else return (Just (expr,wellDefined expr)))
 
   -- Try to get an example of another point, which is finite, and at