From 2c2705628317698709c3113bf6c11acdebc02ec7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 25 Oct 2017 10:24:49 -0700
Subject: [PATCH] disable model example pending C compliance or C99 or whatever
 adjustment

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/c/test_capi.c | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
index 433c7ebcf..178b77b86 100644
--- a/examples/c/test_capi.c
+++ b/examples/c/test_capi.c
@@ -2844,9 +2844,9 @@ void fpa_example() {
    \brief Demonstrates some basic features of model construction
 */
 
+#if 0
 void mk_model_example() {
     printf("\nmk_model_example\n");
-    LOG_MSG("mk_model_example");
     Z3_context ctx = mk_context();
     // Construct empty model
     Z3_model m = Z3_mk_model(ctx);
@@ -2973,7 +2973,7 @@ void mk_model_example() {
         printf("a+b did not evaluate to expected value\n");
         exit(1);
     }
-
+    
     // Evaluate c[0] + c[1] + c[2] under model
     Z3_ast c0 = Z3_mk_select(ctx, cApp, zeroNumeral);
     Z3_ast c1 = Z3_mk_select(ctx, cApp, oneNumeral);
@@ -3009,6 +3009,7 @@ void mk_model_example() {
     Z3_model_dec_ref(ctx, m);
     Z3_del_context(ctx);
 }
+#endif
 
 /*@}*/
 /*@}*/
@@ -3058,6 +3059,6 @@ int main() {
     substitute_example();
     substitute_vars_example();
     fpa_example();
-    mk_model_example();
+//    mk_model_example();
     return 0;
 }