From a7f89dcdd2faabffd980d16326f15f9304fdca2e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@microsoft.com>
Date: Thu, 20 Dec 2012 12:54:44 +0000
Subject: [PATCH] Move Z3_get_implied_equalities from v3 to v4 ml api as it now
 needs Z3_solver type

---
 src/api/z3_api.h | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index e8306bfb6..98bde7bcf 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6924,12 +6924,15 @@ END_MLAPI_EXCLUDE
         );
 
     /*@}*/
-    
+#endif
+
+
     /**
        @name Deprecated Constraints API
     */
     /*@{*/
 
+#ifdef CorML3
     /**
        \brief Set the SMTLIB logic to be used in the given logical context.
        It is incorrect to invoke this function after invoking
@@ -7111,7 +7114,9 @@ END_MLAPI_EXCLUDE
         __out Z3_model * m, __out Z3_ast* proof, 
         __inout unsigned* core_size, __inout_ecount(num_assumptions) Z3_ast core[]
         );
+#endif
 
+#ifdef CorML4
     /**
        \brief Retrieve congruence class representatives for terms.
 
@@ -7142,7 +7147,9 @@ END_MLAPI_EXCLUDE
         __in_ecount(num_terms) Z3_ast const terms[],
         __out_ecount(num_terms) unsigned class_ids[]
         );
+#endif
 
+#ifdef CorML3
     /**
        \brief Delete a model object.