Opened 5 years ago

Closed 5 years ago

#57 closed defect (duplicate)

Build error in divine-smt

Reported by: Marek Chalupa Owned by: mornfall
Priority: major Milestone: 5.0
Component: other Keywords: build, divine-smt
Cc:

Description

I downloaded the current divine (29c9e5ef04df00) via darcs, tried to build it and I'm getting this error:

Scanning dependencies of target divine-smt
[ 2%] Building CXX object divine/CMakeFiles/divine-smt.dir/smt/builder-smtlib.cpp.o
[ 2%] Building CXX object divine/CMakeFiles/divine-smt.dir/smt/builder-stp.cpp.o
[ 2%] Building CXX object divine/CMakeFiles/divine-smt.dir/smt/builder-z3.cpp.o
/var/tmp/xchalup4/divine/divine/smt/builder-z3.cpp:82:23: error: no member named 'zext' in

namespace 'z3'

? z3::zext( arg, bw - childbw )


/var/tmp/xchalup4/divine/divine/smt/builder-z3.cpp:87:23: error: no member named 'sext' in

namespace 'z3'

? z3::sext( arg, bw - childbw )


/var/tmp/xchalup4/divine/divine/smt/builder-z3.cpp:134:40: error: no member named 'srem' in

namespace 'z3'; did you mean 'drem'?

case sym::Op::SRem: return z3::srem( a, b );

~
drem

/usr/include/x86_64-linux-gnu/bits/mathcalls.h:185:13: note: 'drem' declared here
MATHCALL (drem (_Mdouble_ x, _Mdouble_ y));


/var/tmp/xchalup4/divine/divine/smt/builder-z3.cpp:135:40: error: no member named 'urem' in

namespace 'z3'; did you mean 'drem'?

case sym::Op::URem: return z3::urem( a, b );

~
drem

/usr/include/x86_64-linux-gnu/bits/mathcalls.h:185:13: note: 'drem' declared here
MATHCALL (drem (_Mdouble_ x, _Mdouble_ y));


/var/tmp/xchalup4/divine/divine/smt/builder-z3.cpp:136:44: error: no member named 'shl' in

namespace 'z3'

case sym::Op::Shl: return z3::shl( a, b );


/var/tmp/xchalup4/divine/divine/smt/builder-z3.cpp:137:44: error: no member named 'ashr' in

namespace 'z3'

case sym::Op::AShr: return z3::ashr( a, b );


/var/tmp/xchalup4/divine/divine/smt/builder-z3.cpp:138:44: error: no member named 'lshr' in

namespace 'z3'

case sym::Op::LShr: return z3::lshr( a, b );


7 errors generated.
make[6]: * [divine/CMakeFiles/divine-smt.dir/build.make:89: divine/CMakeFiles/divine-smt.dir/smt/builder-z3.cpp.o] Error 1

Change History (1)

comment:1 Changed 5 years ago by Marek Chalupa

Resolution: duplicate
Status: newclosed

This is a duplicate of https://divine.fi.muni.cz/trac/ticket/49, I haven't noticed it before.

Note: See TracTickets for help on using tickets.