32-bit build issues

[jamesjer]

After building z3 4.8.15 for Fedora, we found that cppcheck failed to build on 32-bit platforms. See this failed build on 32-bit x86. The errors look like this:

/usr/include/z3/z3++.h: In function 'z3::expr z3::pble(const expr_vector&, const int*, int)':
/usr/include/z3/z3++.h:2336:26: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2336 |         context& ctx = es[0].ctx();
      |                          ^
/usr/include/z3/z3++.h:2336:26: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h: In function 'z3::expr z3::pbge(const expr_vector&, const int*, int)':
/usr/include/z3/z3++.h:2344:26: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2344 |         context& ctx = es[0].ctx();
      |                          ^
/usr/include/z3/z3++.h:2344:26: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h: In function 'z3::expr z3::pbeq(const expr_vector&, const int*, int)':
/usr/include/z3/z3++.h:2352:26: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2352 |         context& ctx = es[0].ctx();
      |                          ^
/usr/include/z3/z3++.h:2352:26: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h: In function 'z3::expr z3::atmost(const expr_vector&, unsigned int)':
/usr/include/z3/z3++.h:2360:26: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2360 |         context& ctx = es[0].ctx();
      |                          ^
/usr/include/z3/z3++.h:2360:26: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h: In function 'z3::expr z3::atleast(const expr_vector&, unsigned int)':
/usr/include/z3/z3++.h:2368:26: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2368 |         context& ctx = es[0].ctx();
      |                          ^
/usr/include/z3/z3++.h:2368:26: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h: In function 'z3::expr z3::sum(const expr_vector&)':
/usr/include/z3/z3++.h:2376:28: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2376 |         context& ctx = args[0].ctx();
      |                            ^
/usr/include/z3/z3++.h:2376:28: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h: In function 'z3::expr z3::distinct(const expr_vector&)':
/usr/include/z3/z3++.h:2385:28: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2385 |         context& ctx = args[0].ctx();
      |                            ^
/usr/include/z3/z3++.h:2385:28: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h: In function 'z3::expr z3::concat(const expr_vector&)':
/usr/include/z3/z3++.h:2414:24: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2414 |             return args[0];
      |                        ^
/usr/include/z3/z3++.h:2414:24: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h:2416:28: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2416 |         context& ctx = args[0].ctx();
      |                            ^
/usr/include/z3/z3++.h:2416:28: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h:2418:37: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2418 |         if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
      |                                     ^
/usr/include/z3/z3++.h:2418:37: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h:2421:41: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2421 |         else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
      |                                         ^
/usr/include/z3/z3++.h:2421:41: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h: In function 'z3::expr z3::mk_xor(const expr_vector&)':
/usr/include/z3/z3++.h:2451:22: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 2451 |         expr r = args[0];
      |                      ^
/usr/include/z3/z3++.h:2451:22: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h: In member function 'void z3::solver::cube_iterator::inc()':
/usr/include/z3/z3++.h:2774:49: error: ambiguous overload for 'operator[]' (operand types are 'z3::expr_vector' {aka 'z3::ast_vector_tpl<z3::expr>'} and 'int')
 2774 |                 if (m_cube.size() == 1 && m_cube[0].is_false()) {
      |                                                 ^
/usr/include/z3/z3++.h:2774:49: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~
/usr/include/z3/z3++.h: In function 'z3::expr z3::re_intersect(const expr_vector&)':
/usr/include/z3/z3++.h:3807:28: error: ambiguous overload for 'operator[]' (operand types are 'const z3::expr_vector' {aka 'const z3::ast_vector_tpl<z3::expr>'} and 'int')
 3807 |         context& ctx = args[0].ctx();
      |                            ^
/usr/include/z3/z3++.h:3807:28: note: candidate: 'operator[](Z3_ast_vector {aka _Z3_ast_vector*}, int)' (built-in)
/usr/include/z3/z3++.h:546:11: note: candidate: 'T z3::ast_vector_tpl<T>::operator[](unsigned int) const [with T = z3::expr]'
  546 |         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
      |           ^~~~~~~~

Changing the indices to be explicitly unsigned seems to resolve the issue; e.g., change es[0].ctx() to es[0U].ctx(). I don't know if that is the best solution.

[NikolajBjorner]

Changing to 0u is an option.

Maybe other option is to allow operator[] take int as argument instead of unsigned?
The obvious overflow could happen, but be checked.

[NikolajBjorner]

I am trying to resolve this one by using 0u. Changing to "int" could cause other issues.