Running CPAChecker under windows with MathSat

[Dan]

Hello,

I am trying to run CPAChecker with the sv-comp16 configuration (for this I need MathSat, so, I have tried to install it on top of the CPAchecker-1.6.1-windows installation). 

I have downloaded MathSat5 from "http://mathsat.fbk.eu/download.html" and copied the "mathsat.dll" and "mathsat.lib" into "cpachecker\lib\java\runtime". I have renamed mathsat.dll into mathsat5j.dll.

CPAChecker complains that:

---

Warning: Skipping one analysis because the configuration file config\components\sv-comp16--02-valueAnalysis-itp.properties is invalid (The SMT solver MATHSAT5 is not available on t

his machine because of missing libraries (D:\tools\CPAchecker-1.6.1-windows\lib\java\runtime\mathsat5j.dll: Can't find dependent libraries). You may experiment with SMTInterpol by

setting solver.solver=SMTInterpol.) (SolverContextFactory.generateContext, WARNING)

---

What am I doing wrong? Is there documentation about how to install (additionally) the MathSat into CPAChecker such that the sv-comp16 configuration can be used?

Thank you!

With best regards,

Dan

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear Dan,

thank you for your interest in CPAchecker!

While CPAchecker itself is platform-independent, some of its
(optional) libraries are not, and unfortunately there is only little
Windows expertise in the CPAchecker development team.
We try our best to make CPAchecker runnable on non-Linux platforms,
but we cannot guarantee anything there.

So you are invited to try running CPAchecker on Windows, and if you
find problems or even bugs, please report them, we will try to fix
them. But I would like to let you know that your experience might not
be as smooth as when running CPAchecker on Linux.

I think this cannot work directly, because you need to compile a
wrapper for MathSAT to make it callable from Java (this is what we
call "mathsat5j"). Just renaming the library won't fix this.

The integration of MathSAT into CPAchecker is handled in a separate
project called JavaSMT (https://github.com/sosy-lab/java-smt).
There is the source code for the wrapper and a script to compile it:
> https://github.com/sosy-lab/java-smt/blob/master/lib/native/source/libmathsat5j/compile.sh
Unfortunately,
>
there is no such ready-to-use script for Windows, and
documentation for building this wrapper is currently still missing
(https://github.com/sosy-lab/java-smt/issues/44).

So if you would like to use CPAchecker with MathSAT on Windows,
you would need to adapt the compilation of this wrapper to Windows.
If you do so, or if you have further questions on this, it would be
best to contact the JavaSMT project directly, for example in the
above-mentioned issue (I guess they would like to merge build tools
for Windows if contributed).

Kind regards, Philipp
- --
Philipp Wendler
Lehrstuhl für Softwaresysteme
Universität Passau
Raum IM 110 - Tel.: 0851/509-3093
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.22 (GNU/Linux)

iQIcBAEBAgAGBQJXssgGAAoJEGLA94wxqd6MWH4P+wVs+Sch3Ly894uQxcXdpyO1
542mPVhjvLb8jrGf9ljOcMXx7XTJ8xAX1j1ttNw1wF0QcAtG6Z8FPLi+1jM+YRE9
dOLRr88zb5EFcEfENtsbsbX15O7Dg8V2znPHCp3aY0dU6Sp+Kv34UH9cBYkCBFTd
hBlVVLfBRqgWGYjJivdJy9umlx6SMZaL8LCZrXwzIizz5NdvjEXjpXq1HTEd4WXB
uPgP2PNAIIIewOPo6zan9uFvCAdeIXfE98EGR0jisd8jv+cWvZ6IL0pqPu1OuiT5
iHvvbArf03KN3niK+iZmoTbMlz7M4vi2paeiv+2IH+VnBoNWLf16mt+z4R5I0TJi
UMNHxcg79lMcagSVodB3/hfXSyzjL6hjbXmRi6h4d757p3tGVjf4emk/9kBkKIoz
pGJ3rHIKSf7k35ltQ05uJAvsl40jiNtTO1DL6MVwnAnAHh+/tXLM6B8paRuYHv6L
vo6/H0TOSFseKuXpKWv+VtKOXxED/UUlB3X5X6KjMuLYZTOUQTZceJo62fhqvt6U
ML4sNW9RiPV2+NnLiTEYZ4xQn05UH2ncdONGjv6IamWIdBlC0u+ERMukCT7OLr6k
HPS0T67kMs4WRYochKSl9iKNI/daG81ICUNLnHGs3R+Y8LRfxjsPDHyvViI28gtZ
lhSQkxZus242p0g27P9u
=cvcF
-----END PGP SIGNATURE-----

[George Karpenkov]

Hello Dan,

Philipp's answer is very good,

I just would like to add that I think you would be better of running CPAchecker

inside a Virtualbox with Ubuntu, since that would be very easy to set up.

Regards,

George