fix #6114

Z3Prover · Jul 18, 2022 · 393c63f · 393c63f
1 parent 527914d
commit 393c63f
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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++)