From 76dec85c93233922d4c79eb98c2b6c237e8c3b15 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Mar 2018 15:41:53 -0700
Subject: [PATCH] use stdbool #1526 instead of int

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/update_api.py   |  7 ++++++-
 src/api/z3_api.h        |  2 +-
 src/api/z3_replayer.cpp | 10 ++++++++++
 src/api/z3_replayer.h   |  1 +
 4 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/scripts/update_api.py b/scripts/update_api.py
index 18878d6ea..0a86db18d 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -957,11 +957,16 @@ def def_API(name, result, params):
                 log_c.write(" }\n")
                 log_c.write("  Au(a%s);\n" % sz)
                 exe_c.write("in.get_uint_array(%s)" % i)
-            elif ty == INT or ty == BOOL:
+            elif ty == INT:
                 log_c.write("U(a%s[i]);" % i)
                 log_c.write(" }\n")
                 log_c.write("  Au(a%s);\n" % sz)
                 exe_c.write("in.get_int_array(%s)" % i)
+            elif ty == BOOL:
+                log_c.write("U(a%s[i]);" % i)
+                log_c.write(" }\n")
+                log_c.write("  Au(a%s);\n" % sz)
+                exe_c.write("in.get_bool_array(%s)" % i)
             else:
                 error ("unsupported parameter for %s, %s, %s" % (ty, name, p))
         elif kind == OUT_ARRAY:
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 50ed85c70..ab570581b 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -82,7 +82,7 @@ DEFINE_TYPE(Z3_rcf_num);
 /**
    \brief Z3 Boolean type. It is just an alias for \c int.
 */
-typedef int Z3_bool;
+typedef bool Z3_bool;
 
 /**
    \brief Z3 string type. It is just an alias for \ccode{const char *}.
diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp
index 1515e6df7..fde9b1f48 100644
--- a/src/api/z3_replayer.cpp
+++ b/src/api/z3_replayer.cpp
@@ -630,6 +630,12 @@ struct z3_replayer::imp {
         return m_int_arrays[idx].c_ptr();
     }
 
+    bool * get_bool_array(unsigned pos) const {
+        check_arg(pos, UINT_ARRAY);
+        unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
+        return reinterpret_cast<bool*>(m_unsigned_arrays[idx].c_ptr());
+    }
+
     Z3_symbol * get_symbol_array(unsigned pos) const {
         check_arg(pos, SYMBOL_ARRAY);
         unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
@@ -761,6 +767,10 @@ int * z3_replayer::get_int_array(unsigned pos) const {
     return m_imp->get_int_array(pos);
 }
 
+bool * z3_replayer::get_bool_array(unsigned pos) const {
+    return m_imp->get_bool_array(pos);
+}
+
 Z3_symbol * z3_replayer::get_symbol_array(unsigned pos) const {
     return m_imp->get_symbol_array(pos);
 }
diff --git a/src/api/z3_replayer.h b/src/api/z3_replayer.h
index e1b32af75..b81659945 100644
--- a/src/api/z3_replayer.h
+++ b/src/api/z3_replayer.h
@@ -51,6 +51,7 @@ public:
 
     unsigned * get_uint_array(unsigned pos) const;
     int * get_int_array(unsigned pos) const;
+    bool * get_bool_array(unsigned pos) const;
     Z3_symbol * get_symbol_array(unsigned pos) const;
     void ** get_obj_array(unsigned pos) const;