0

I am trying to compile the SMT solver Z3 (Version 4.5.0) from Microsoft Research on a Solaris 10 (Sparc) with Solaris Studio 12.3 (and this is due to constraints that I cannot change, so please do not hint to gcc/g++).

I already had to make some (more or less trivial) code changes in order to come to the error I am opposed with now:

"../src/util/map.h", line 54: Error: Formal argument p of type const std::pair<expr*, int>& in call to pair_hash<obj_ptr_hash<expr>, int_hash>::operator()(const std::pair<expr*, int>&) const is being passed const std::pair<expr*, bool>.
"../src/util/hashtable.h", line 155:     Where: While instantiating "table2map<default_map_entry<std::pair<expr*, bool>, bool>, pair_hash<obj_ptr_hash<expr>, int_hash>, default_eq<std::pair<expr*, bool>>>::entry_hash_proc::operator()(const _key_data<std::pair<expr*, bool>, bool>&) const".
"../src/util/hashtable.h", line 155:     Where: Instantiated from core_hashtable<default_map_entry<std::pair<expr*, bool>, bool>, table2map<default_map_entry<std::pair<expr*, bool>, bool>, pair_hash<obj_ptr_hash<expr>, int_hash>, default_eq<std::pair<expr*, bool>>>::entry_hash_proc, table2map<default_map_entry<std::pair<expr*, bool>, bool>, pair_hash<obj_ptr_hash<expr>, int_hash>, default_eq<std::pair<expr*, bool>>>::entry_eq_proc>::get_hash(const _key_data<std::pair<expr*, bool>, bool>&) const.
"../src/util/hashtable.h", line 350:     Where: Instantiated from non-template code.
1 Error(s) and 33 Warning(s) detected.
*** Error code 2
The following command caused the error:
CC -D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE  -xldscope=hidden -c -xarch=sse2 -xvector=simd -D_NO_OMP_ -D _EXTERNAL_RELEASE -xO3 -xregs=frameptr -D_SUNOS_ -KPIC -xalias_level=any -features=zla -I../src/ast/rewriter/bit_blaster -I../src/ast/rewriter -I../src/ast -I../src/util -I../src/math/polynomial -I../src/math/automata -I../src/ast/simplifier -I../src/ast/macros -I../src/ast/normal_forms -I../src/cmd_context -I../src/solver -I../src/model -I../src/tactic -I../src/interp -I../src/smt/proto_model -I../src/smt/params -I../src/ast/pattern -I../src/parsers/smt2 -I../src/parsers/util -I../src/ast/substitution -I../src/math/grobner -I../src/math/euclid -I../src/math/simplex -I../src/ast/proof_checker -I../src/ast/fpa -osmt/smt_quick_checker.o ../src/smt/smt_quick_checker.cpp
make: Fatal error: Command failed for target `smt/smt_quick_checker.o'
bash-3.2$

The code causing the error can be found here at line 54.

I already poked around with a cast to std::pair<expr*, int>, but as this is code used with different types, this lead to a similar error with unsigned.

Can anybody help me with this error?

4

0 回答 0