Daniel Dietsch comments

Results 157 comments of


                                            Daniel Dietsch

Incorrect Büchi program while using LTLAutomizerCInline toolchain

Adding support for multi-threaded programs is hard for numerous reasons. It wont be done quickly, but possibly this year.

Boogie variables beginning with a period are disallowed

I will have a look.

Boogie variables beginning with a period are disallowed

For completeness sake: The SMT-LIB Standard Version 2.6, Sec 3.1, p24, Symbols, last paragraph: > Simple symbols starting with the character @ or . are reserved for solver use.^4 Solvers...

rcfgbuilder.add.additional.assume.for.each.assert true may produce confusing / spurious results

You can prevent this behavior by disabling the RCFG option "assume assert". The example should then contain both counterexamples. For other cases: What qualifies as dead code?

rcfgbuilder.add.additional.assume.for.each.assert true may produce confusing / spurious results

Is this also sufficient for your dead code problem?

rcfgbuilder.add.additional.assume.for.each.assert true may produce confusing / spurious results

This sounds reasonable. I am not sure if we have some settings that depend on this value.

UReqCheck usage problem

Hi @IridescentL, I am unsure what you are trying to do. Do you want to disable vacuity and consistency checks? If you just want to compare speeds, you might want...

Broken Support for Functions Without Parameters

I do not see the connection to #442. We are currently translating this function to a 0-ary SMT function: ``(declare-fun myFunction () Int)`` Do you propose that we identify 0-ary...

Ultimate crashes with OOM for array[8192]

see #415: probably the same reason, just a different symptom

Performance Improvements around hashCode and equals

The [changes between these commits](https://github.com/ultimate-pa/ultimate/compare/0612a5f..3902331) do not simply introduce `hashJenkins`, they also change some things slightly (somewhat bigger `Condition`, hashJenkins that does not consider other fields anymore in `Transition`). This...