Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ResultNotifier messages are not consistent with actual result messages #6

Closed
danieldietsch opened this issue Oct 27, 2015 · 4 comments

Comments

@danieldietsch
Copy link
Member

danieldietsch commented Oct 27, 2015

As seen in Jan Hättig's presentation today, the result notifier states that there is no result when the real result is actually safe. Either remove the result notifier or fix this contradiction.

@Heizmann
Copy link
Member

It seems that not all toolchains are affected. E.g., if I use the Automizer toolchain, I obtain the following.
2015-10-28 01:47:44,575 INFO [ResultNotifier.java:137]: RESULT: Ultimate proved your program to be correct!
However, I agree that the ResultNotifier has to be revised some day. (Problems? E.g., how do we summarize several positive results?)

jhoenicke pushed a commit that referenced this issue Mar 18, 2016
In the lira case, bounds for integer variables might not be integers.  In this
case, we normalise these bounds by rounding and choosing the appropriate value.
If the interval becomes singular, we return the only possible value.
This fixes #6.
@schillic
Copy link
Member

When using the command line interface (tested with the binary release 0.1.19) and using the AutomataScriptInterpreter (may also occur with other toolchains; not tested) on an automata file (*.ats) that contains an assertion (assert(...)), upon (successful) termination Ultimate adds the following result output: Ultimate could not prove your program: Assertion holds

@danieldietsch
Copy link
Member Author

What is the expected behavior?

  • No message
  • A message saying something like "Ultimate proved your program to be correct"
  • Something automata-specific, like "Ultimate proved your automata to be correct"

Do you have a sample input file, settings file, toolchain file (just something from our repo is enough, you do not need to attach it).

@schillic
Copy link
Member

I do not know the expected behavior because I do not know the spec of the CLI.
It looks like "No message" would be fine because there is already a line with the (correct) result.

To reproduce, run the CLI with the toolchain AutomataScriptInterpreter.xml and this example, but I expect any example with assertions should do.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants