From 393c63fe0cc5afe1c32b2a46f154d8e0bce267e6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Jul 2022 09:33:39 -0700
Subject: [PATCH] fix #6114
---
examples/c++/example.cpp | 4 ++--
src/api/c++/z3++.h | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 0217c5cca..c71c3ff2f 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -929,8 +929,8 @@ void enum_sort_example() {
sort s = ctx.enumeration_sort("enumT", 3, enum_names, enum_consts, enum_testers);
// enum_consts[0] is a func_decl of arity 0.
// we convert it to an expression using the operator()
- expr a = enum_consts[0]();
- expr b = enum_consts[1]();
+ expr a = enum_consts[0u]();
+ expr b = enum_consts[1u]();
expr x = ctx.constant("x", s);
expr test = (x==a) && (x==b);
std::cout << "1: " << test << std::endl;
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index fc0601fe5..8aaeb31ab 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2894,7 +2894,7 @@ namespace z3 {
if (n == 0)
return ctx().bool_val(true);
else if (n == 1)
- return operator[](0);
+ return operator[](0u);
else {
array<Z3_ast> args(n);
for (unsigned i = 0; i < n; i++)