v0.1.19

Features

Automata Library

• added union operation
• added isFinite operation

Misc

• first working prototype of EQ domain with array support (see #159, #195)
• preliminary implementation of HeapSeparator in IcfgTransformation (see #197)
• preliminary support for error automata in Ultimate Automizer (see #182)
• support for new requirements pattern InitializationPattern: Allows to specify types of variables s.t. former atomic propositions are not atomic anymore
• totalize now supports nondeterministic automata
• unsat-core-free relevance computation now also for call and return

Bugfixes

TreeAutomizer

• fix to HCHoareTripleChecker (in order to fix generalization of interpolant automata in TreeAutomizer) some cleanup

Misc

• fix backtranslation of to_fp (closes #198)
• prevent multiple windows from appearing by not using a parent for the dialog (closes #196)
• fix: fault localization should compute error pre-/postcondition
• fix srParse test cases
• fix small bug in IcfgTransformerSequence: did not add return transitions last
• fix bug in icfgtransformation mapelimination: transform both transformulas of a return transition (also, be less verbose)
• fix bug in absint: futureicfg did check for wrong call/return types
• omit problematic simplifications for store and select
• various fixes for LA Mohr and LA Werner

Plumbing

• add new preferences MAP_ELIMINATION_NO_EQUALITY and MAP_ELIMINATION_EQUALITY to IcfgTransformation
• Hoare triple checkers are more modular
• add log levels to ILogger mock
• add IncrementalImplicationChecker
• Add more logging output for assertion orders
• explain relevance information in output

Known Issues

• README and Website usage instructions outdated (see #135)
• Startup with generated binary ./Ultimate stalls if no X display is available