#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 6 years ago by Marek Chalupa

Resolution:	→ duplicate
Status:	new → closed

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.