mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fix #6114

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-18 09:33:39 -07:00
parent 527914db05
commit 393c63fe0c
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
examples/c++/example.cpp
View file

@ -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;

2
src/api/c++/z3++.h
View file

@ -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++)