How to run from a release?

[nekketsuuu]

Hi.
I'm new to ultimate, and I tried to use Ultimate Automizer which is downloaded from a release.
Specifically, I downloaded UltimateAutomizer-linux.zip and unzip it.

However, although README in this zip said "This archive contains a set of property files located in the directory props/", there is no such a directory and *.prp files.
It would be this directory in the repository, so I copy and paste it manually.

Then I make a very simple test case,

int main(void) { return 0; }

and execute ./Ultimate.py props/Termination.prp 64bit test/test1.c, but it failed with a following error message:

$ ./Ultimate.py props/Termination.prp 64bit test/test1.c 
Checking for termination
Using default analysis
Version f7c3ed31
Calling Ultimate with: java -Xmx12G -Xms1G -jar plugins/org.eclipse.equinox.launcher_1.3.100.v20150511-1540.jar -data @user.home/.ultimate -tc /home/nek/github/ultimate/UAutomizer-linux-SV-COMP-2017/AutomizerTermination.xml -i test/test1.c -s /home/nek/github/ultimate/UAutomizer-linux-SV-COMP-2017/svcomp-Termination-64bit-Automizer_Default.epf
..........................................................................................................................................................................................................
Execution finished normally
Retrying with bit-precise analysis
Using bit-precise analysis
No suitable settings file found using Termination*64bit*_Bitvector
ERROR: UNSUPPORTED PROPERTY

Actually, svcomp-Termination-{32bit, 64bit}-Automizer_Default.epf is in the archive, but svcomp-Termination-{32bit, 64bit}-Automizer_Bitvector.epf is not.

Am I missed something?

I also read this wiki article, but this article wouldn't be related to my question.

Environment: x86_64, Ubuntu 14.04 LTS, bash, python 2.7.6, java 1.8.0_121

[danieldietsch]

Hi,
the README is indeed wrong, I am sorry for this. But copying the properties from the SV-COMP repository is exactly right and your example program works for me (result: true). Your environment also looks fine. It may be the case that your glibc is different and the supplied version of z3 does therefore not work for you (which would be our fault).

Could you run Ultimate with the --full-output option and paste the result?
./Ultimate.py --full-output props/Termination.prp 64bit test/test1.c

The wiki article you read is for our students so they can setup their development environment. We should perhaps preface this with this information.

[nekketsuuu]

Thank you for your reply!

glibc: GNU C Library (Ubuntu EGLIBC 2.19-0ubuntu6.9) stable release version 2.19, by Roland McGrath et al.

Result with --full-output (but the diff is only the number of dots...)

$ ./Ultimate.py props/Termination.prp 64bit test/test1.c --full-output
Checking for termination
Using default analysis
Version f7c3ed31
Calling Ultimate with: java -Xmx12G -Xms1G -jar plugins/org.eclipse.equinox.launcher_1.3.100.v20150511-1540.jar -data @user.home/.ultimate -tc /home/nek/github/ultimate/UAutomizer-linux-SV-COMP-2017/AutomizerTermination.xml -i test/test1.c -s /home/nek/github/ultimate/UAutomizer-linux-SV-COMP-2017/svcomp-Termination-64bit-Automizer_Default.epf
...........................................................................................................................................................................................................
Execution finished normally
Retrying with bit-precise analysis
Using bit-precise analysis
No suitable settings file found using Termination*64bit*_Bitvector
ERROR: UNSUPPORTED PROPERTY

I have other Z3 such as ~/anaconda3/bin/z3, so I tried to set $PATH so that which z3 outputs ultimate/UAutomizer-linux-SV-COMP-2017/z3, but the result is the same.
Maybe it's not a matter of Z3?

[danieldietsch]

Can you try and run it without the wrapper script?
java -Xmx12G -Xms1G -jar plugins/org.eclipse.equinox.launcher_1.3.100.v20150511-1540.jar -data @user.home/.ultimate -tc /home/nek/github/ultimate/UAutomizer-linux-SV-COMP-2017/AutomizerTermination.xml -i test/test1.c -s /home/nek/github/ultimate/UAutomizer-linux-SV-COMP-2017/svcomp-Termination-64bit-Automizer_Default.epf

[nekketsuuu]

It wrote a large log: gist here.

Around line 116, a Z3 error occurred.

[danieldietsch]

Ok, this looks promising so far.
The log indicates that z3 just crashes with no useful output.
Can you delete / rename the z3 binary in the Ultimate folder and use the one you have in your path?

[nekketsuuu]

Oh, it succeeded!
Thank you for your big help!

[danieldietsch]

No problem -- we really have to revise our readme and fix this z3 issue. Continuing this in #104 and #105