From 6e18f44d991344fc444b21c13e4c2233334ab6d8 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@yahoo.com>
Date: Wed, 22 Oct 2014 10:42:23 -0700
Subject: [PATCH] fixed error check in read_interpolation_problem

---
 src/api/api_interp.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index dbf68da38..63ecc6c24 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -617,7 +617,7 @@ extern "C" {
         }
 
         for (unsigned j = 0; j < num - 1; j++)
-            if (read_parents[j] == SHRT_MIN){
+            if (read_parents[j] == SHRT_MAX){
             read_error << "formula " << j + 1 << ": unreferenced";
             goto fail;
             }
@@ -717,4 +717,4 @@ Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx,
                                __in unsigned incremental,
                                __in unsigned num_theory,
                                __in_ecount(num_theory) Z3_ast *theory);
-#endif
\ No newline at end of file
+#endif