search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
198 stars 41 forks source link

Problem with validator from SVCOMP 2021 #549

Closed hernanponcedeleon closed 3 years ago

hernanponcedeleon commented 3 years ago

Hi,

I'm using the version of UAutomizer from the archive2021 repo of SVCOMP and I'm getting and error when trying to validate a witness. I'm running the following cmd

./Ultimate.py --spec ~/git/sv-benchmarks/c/properties/unreach-call.prp --file ~/git/sv-benchmarks/c/pthread-wmm/mix000_power.oepc.i --architecture 32bit --validate ~/git/Dat3M/output/witness.graphml

which results in

Checking for ERROR reachability
Using default analysis
Version 7b2dab56
Calling Ultimate with: /usr/bin/java -Dosgi.configuration.area=/Users/ponce/git/forks/archives-2021/2021/UAutomizer-linux/data/config -Xmx15G -Xms4m -jar /Users/ponce/git/forks/archives-2021/2021/UAutomizer-linux/plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar -data @noDefault -ultimatedata /Users/ponce/git/forks/archives-2021/2021/UAutomizer-linux/data -tc /Users/ponce/git/forks/archives-2021/2021/UAutomizer-linux/config/AutomizerReachWitnessValidation.xml -i /Users/ponce/git/sv-benchmarks/c/pthread-wmm/mix000_power.oepc.i /Users/ponce/git/Dat3M/output/witness.graphml -s /Users/ponce/git/forks/archives-2021/2021/UAutomizer-linux/config/svcomp-Reach-32bit-Automizer_Default.epf --cacsl2boogietranslator.entry.function main --traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg false
.................................................................................................................................................................................
Execution finished normally
Using bit-precise analysis
Retrying with bit-precise analysis
Calling Ultimate with: /usr/bin/java -Dosgi.configuration.area=/Users/ponce/git/forks/archives-2021/2021/UAutomizer-linux/data/config -Xmx15G -Xms4m -jar /Users/ponce/git/forks/archives-2021/2021/UAutomizer-linux/plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar -data @noDefault -ultimatedata /Users/ponce/git/forks/archives-2021/2021/UAutomizer-linux/data -tc /Users/ponce/git/forks/archives-2021/2021/UAutomizer-linux/config/AutomizerReachWitnessValidation.xml -i /Users/ponce/git/sv-benchmarks/c/pthread-wmm/mix000_power.oepc.i /Users/ponce/git/Dat3M/output/witness.graphml -s /Users/ponce/git/forks/archives-2021/2021/UAutomizer-linux/config/svcomp-Reach-32bit-Automizer_Bitvector.epf --cacsl2boogietranslator.entry.function main --traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg false
...................................................................................................................................................................................
Execution finished normally
Writing output log to file Ultimate.log
Result:
ERROR: ExceptionOrErrorResult: NullPointerException: null

Attached are the two used files (taks + witness) + the log from UAutomizer. Archive.zip

Am I missing any option flag maybe?

danieldietsch commented 3 years ago

@hernanponcedeleon there are multiple issues here.

hernanponcedeleon commented 3 years ago

@danieldietsch: the problem with z3 is probably that this is the binary for the competition, i.e. Linux environment, and I'm trying to run this on MacOS. However a have z3 installed in my laptop. Is there any way to set the path to the solver (I could not find anything in the help)?

danieldietsch commented 3 years ago

Yeah, it is somewhat awkward -- the easiest is probably just to rename the binary we supply, then it will automatically take the one from your PATH.

hernanponcedeleon commented 3 years ago

That worked. From my side everything is ok. I did not close the issue based on the tags you added, but feel free to close it.