How to point to a SMT solver on Windows? #203
Comments
|
-p C:\Users\<user>\Documents\z3-4.8.8-x64-win\bin
This is folder, it should point to an executable, eg -p
C:\Users\<user>\Documents\z3-4.8.8-x64-win\bin\z3.exe
|
|
Thank you for your response, monperrus! Unfortunately, the issue persists even when pointing to the executable, throwing the previously posted error message. Could the Java version be the problem? In the output before the exception occurs, it displays:
Then it displays PATH and all paths in there, followed by the exception. Lastly, it displays the usage with all parameters. |
|
Sorry for closing the issue, I am used to have an upload button next to the comment button. I have attached the full log of NOPOL as a text file to this comment. EDIT: In the text file, the path is C:\Users<user>\nopol\nopol>, but the issue also happens from the C:\Users<user>\nopol\test-projects path from the instructions. |
|
What happens if you debug the problem and add a breakpoint just before the exception? |
|
Thanks again for your response! If I try to setup the project in my IDE, Eclipse, to be able to set break points, I get a different error when running the project with the following configuration:
Even if I was able to set a breakpoint, Java is not one of my main programming languages and I don't know how much I could contribute to solving the issue. Since it is not a requirement for my paper to actually run NOPOL, I might give up on trying to set it up, even if it would be a great enhancement to use it to create my own examples to show how the tool solves different issues giving reality to the theory behind it. |
|
this is a gzoltar bug, probably due to an incorrect classpath.
to make progress, you can try with "--flocal cocospoon" to disable gzoltar
|
|
After adding "--flocal cocospoon", I get this error
As told in the instructions after I downloaded your project examples and did not change any directories, I added for the source code of the project the path "src/main/java" and the tests for that source code is in "src/test/java". Maybe this is the problem because the tests are in a different directory? Out of curiosity, I changed the test class for the parameter -t to "symbolic_examples.symbolic_example_1.NopolExample", which is the source code file and there it runs fine, although it obviously doesn't find statements since it is not include tests:
So the issue seems to be that it isn't able to find the class containing the test cases. Even when I give -t the absolute path to the file I still get the same error. I also tried moving the class file to the same directory of the source code and renaming it, but nonetheless it still yields the same error. Although interestingly, if I move the test file itself to the location of the source code, not renaming it and updating references, I get these messages instead:
So still, it doesn't find the class. What could be the issue here? |
|
This is most likely a classpath problem:
* make sure you have recompiled the project under repair, both the app
and the tests
* make sure to give the right folders as classpath
(-c|--classpath) <classpath>
Define the classpath of the project separated by a path
separator (`:` on Linux).
Must contain the application binary classes (`target/classes`)
Must contain the application test classes (`target/test-classes`)
Must contain the library classes (`lib/junit.jar` for instance)
|
|
Thank you very much for your assistance and bearing with my questions, monperrus! I managed to execute NOPOL for the example test class by fixing the classpath problem with your explanation and solution. Please feel free to close this issue now. |
|
perfect |
Hello, I am writing an academic paper on NOPOL and I am trying to setup the project on Windows 10. I followed all steps up to step 4, but now I seem to be unable to point to a SMT solver and I would greatly appreciate some help.
I decided to go with the SMT solver Z3 and downloaded the pre-built binary z3-4.8.8-x64-win.zip from their releases.
Then, I used the following command lines to execute NOPOL, with my correct username:
However, I am getting an exception and executing NOPOL fails:
Testing revealed that leaving the parameter -p empty causes the same exception as the current path that is provided for the SMT solver. At the path C:\Users<user>\Documents\z3-4.8.8-x64-win\bin, there is the extracted content of the z3-4.8.8-x64-win.zip file. Since the instructions mention that -p should point to a binary path, I chose this path, however, in the example that is provided, a single file is referenced. Yet, in the content of z3-4.8.8-x64-win.zip, there is no binary file, if I see it correctly. There is a z3.exe, a com.microsoft.z3.jar and a z3.py, but no file that resembles the example "z3_for_linux" in NOPOL.
Which file do I have to reference there? I would greatly appreciate some assistance.
The text was updated successfully, but these errors were encountered: