search

pietrobraione / jbse

A symbolic Java virtual machine for program analysis, verification and test generation
http://pietrobraione.github.io/jbse/
GNU General Public License v3.0
102 stars 29 forks source link

Setting Z3 Solver #6

Closed wombatwen closed 6 years ago

wombatwen commented 7 years ago

Hi, I use Eclipse and my OS is win10 x64. I follow the installation guide of Z3 solver and have successfully built Z3 with --java flag. Now I have "com.microsoft.z3.jar", but have no idea how to link jbse with z3 solver. Is there any suggestion?

Thanks,

pietrobraione commented 7 years ago

Hi and sorry for the late answer. JBSE does not link to Z3 via the com.microsoft.z3.jar but by exchanging commands through pipes. You just need to inform JBSE about the location of the z3.exe file by the method jbse.apps.run.RunParameters.setExternalDecisionProcedurePath(String). Maybe you will also need to tweak a bit the COMMANDLINE_LAUNCH_Z3 constant in jbse.apps.run.Run and change it as follows:

 private static final String COMMANDLINE_LAUNCH_Z3   = " /smt2 /in /t:10";

Best, Pietro