compiling z3 4.1 on OS X to use Boogie

Question

I'm trying to install Boogie (22 Oct 2012 version) on Mac OS X 10.8. I downloaded the Boogie from here, and installed Mono 3.4.0. Boogie without the verify option worked fine for me.

Next, I needed to install Z3. I tried the nightly OS X build because I thought that would be simplest, but Boogie gave a lot of errors along the lines of:

Prover error: line 5 column 22: the parameter 'model_v2' was renamed to 'model.v2', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:model.v2' for the full description of the parameter

So I tried to download the source for Z3 version 4.1 and compile it. I ran autoconf, and configure without any problems, but make had many errors:

$ autoconf
$ ./configure
checking for dos2unix... /usr/local/bin/dos2unix
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables...
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking whether make sets $(MAKE)... yes
clang: warning: treating 'c' input as 'c++' when in C++ mode, this behavior is deprecated
checking how to run the C++ preprocessor... g++ -E
configure: creating ./config.status
config.status: creating Makefile

Z3 was configured with success.
Host platform: osx
Arithmetic:    internal

Type 'make' to compile Z3.
$ make
Makefile:271: obj/external/act_cache.d: No such file or directory
Makefile:271: obj/external/add_bounds.d: No such file or directory
Makefile:271: obj/external/add_bounds_tactic.d: No such file or directory
Makefile:271: obj/external/aig.d: No such file or directory
....
(many like this)
....
Makefile:273: obj-test/external/array_property_expander.d: No such file or directory
Makefile:273: obj-test/external/arith_rewriter.d: No such file or directory
Makefile:273: obj-test/external/arith_simplifier_plugin.d: No such file or directory
Makefile:273: obj-test/external/ast.d: No such file or directory
....
(and more like this)
....
Making dependency file 'obj-test/external/bits.d' ...
clang: warning: argument unused during compilation: '-fopenmp'
clang: warning: argument unused during compilation: '-mfpmath=sse'
In file included from test/bits.cpp:5:
In file included from lib/mpz.h:29:
lib/z3_omp.h:23:9: fatal error: 'omp.h' file not found
#include"omp.h"
        ^
1 error generated.

Any idea what could be wrong? My g++ version is: Apple LLVM version 5.0 (clang-500.2.79) (based on LLVM 3.3svn)

EDIT: I followed Christoph's suggestions, and I could start the build successfully, but at some point I got the following errors:

clang: warning: argument unused during compilation: '-mfpmath=sse'
lib/hwf.cpp:27:14: warning: pragma STDC FENV_ACCESS ON is not supported, ignoring pragma [-Wunknown-pragmas]
#pragma STDC FENV_ACCESS ON
             ^
In file included from lib/hwf.cpp:50:
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1388:22: error: expected expression
  return (__m128)__in;
                     ^
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1394:23: error: expected expression
  return (__m128i)__in;
                      ^
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1400:23: error: expected expression
  return (__m128d)__in;
                      ^
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1406:23: error: expected expression
  return (__m128i)__in;
                      ^
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1412:22: error: expected expression
  return (__m128)__in;
                     ^
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1418:23: error: expected expression
  return (__m128d)__in;
                      ^
1 warning and 6 errors generated.

Any ideas?

score 2 · Accepted Answer · edited May 23 '17 at 11:52

2

This one is a bit tricky as Boogie doesn't support the new Z3 (see also here), but the old 4.1.2 version of Z3 doesn't support the new compiler (clang) on OSX 10.9. This is mainly because clang lacks support for OpenMP. We can build this version of Z3 without support for OpenMP though, by adding -D_NO_OMP_ to the CPPFLAGS line in the Makefile, or by running

CPPFLAGS=-D_NO_OMP_ LDFLAGS=-stdlib=libstdc++ ./configure

on the command line (the LDFLAGS setting is required because clang selects an unsuitable standard C++ library by default; see here for details). We then need to replace all occurrences of -fopenmp in the Makefile, e.g., by running

sed -i '' "s/-fopenmp//" Makefile

Once that is done, Z3 4.1.2 should build successfully.

edited May 23 '17 at 11:52

Community

1
1

answered Apr 11 '14 at 11:13

Christoph Wintersteiger

8,234
1
16
30

Thank you! I did as you said, and compilation started. I got a lot of warnings saying argument unused. But at the end, I got a few errors (I've edited my post with the errors, because its too big to fit here) – psquid Apr 11 '14 at 14:59
Apparently the old version of clang doesn't support the -mfpmath switch. I'm using LLVM 5.1 (clang 503.0.38) on OSX 10.9 and it works fine here. As far as I remember, the default compiler on OSX 10.8 was not clang, but gcc, perhaps the easiest way to get it to work is to use that one. Otherwise, could you perhaps update your Xcode command line tools to a newer version if there is one? – Christoph Wintersteiger Apr 11 '14 at 15:13
I updated my xcode to the latest version and it compiled. Thank you very much :) – psquid Apr 11 '14 at 20:03

compiling z3 4.1 on OS X to use Boogie

1 Answers1