eth-sri / fastsmt

Learning to Solve SMT Formulas Fast
Apache License 2.0
85 stars 18 forks source link

Error when compiling Z3 #7

Open DavidAdamczyk opened 3 years ago

DavidAdamczyk commented 3 years ago

Hello, I have question about readme instructions. The second step is compile Z3 version 4.6.2 (5651d00751a1eb40b94db86f00cb7d3ec9711c4d) but I found this error:

In file included from ../src/util/lp/sparse_matrix.h:23,
                 from ../src/util/lp/lu.h:27,
                 from ../src/util/lp/lp_primal_core_solver.h:32,
                 from ../src/util/lp/lp_primal_simplex.h:27,
                 from ../src/util/lp/mps_reader.h:32,
                 from ../src/shell/lp_frontend.cpp:12:
../src/util/lp/permutation_matrix.h: In member function ‘unsigned int* lp::permutation_matrix<T, X>::values() const’:
../src/util/lp/permutation_matrix.h:135:44: error: cannot convert ‘const vector<unsigned int>’ to ‘unsigned int*’ in return
  135 |         unsigned * values() const { return m_permutation; }
      |                                            ^~~~~~~~~~~~~
      |                                            |
      |                                            const vector<unsigned int>
make: *** [Makefile:3998: shell/lp_frontend.o] Chyba 1

The error is probably solved by https://github.com/Z3Prover/z3/issues/1688

So the question is which is the right commit hash (or tag, or Z3 version?)

DavidAdamczyk commented 3 years ago

I found the second one https://github.com/Z3Prover/z3/issues/1622 Please let me know which version/hash is supported with fastsmt.

Vancir commented 3 years ago

I also encountered the same problem when compiling the latest code d2330055e732dacc9423f54a271fdaa235515ad0, but when I checkout to release 4.8.10, it could be compiled successfully.

Environment: Ubuntu 20.04.2 GCC (Ubuntu 9.3.0-17ubuntu1~20.04) 9.3.0