v0.1.15
Pre-release
Pre-release
Features
- AutomataScript is now case-sensitive. Operations are named similar to Java in CamelCase (see #179)
- new MathSAT setting for .epf files and IRefinementStrategy
- add interactive verification prototype via various new plugins
Bugfixes
- fix solver crash because of bvadd with three arguments by translating to response unknown and adding ULTIMATE_VIOLATES_SMT_LIB_STANDARD_AND_SOLVER_COMPLAINS to TraceCheckReasonUnknown (workaround for #185)
- fix StackOverflowException in LA Woelfing
- fix witness xml header: xmlns="http://graphml.graphdrawing.org/xmlns" is correct but incomplete; full boilerplate should be xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://graphml.graphdrawing.org/xmlns http://graphml.graphdrawing.org/xmlns/1.0/graphml.xsd" ( 2d24b14 ) (fixes #112)
- fix build problems by specifying relevant resources for executing builder (closes #167)
- fix API usage: Core should call parseAST(Files[]) for multiple input files that are paresable by the same parser (closes #172)
- fix NPE during toolchainstorage.clear(): do not store null in the storage
- fix compound domain unsoundness (disjunctive compound domain call bug) by using solver to check for inconsistent state (workaround)
Plumbing
Automata Library
- refactoring automata library: do not store alphabet in three sets, but introduce an visibly pushdown alphabet object ( e4bb2b1 )
- remove AA_Accept which is just a copy of AA_Accepts
- add NCSB-based buchi inclusion operation
- minor change in INwaSuccessorStateProvider API
- let BuchiComplementNCSB use new on-demand API
- let SetOfStates provide emtpy stack state
- let BuchiComplementFKV implement new on-demand API
Misc
- added generalized version of IPredicate and TransFormula
- make PredicateTransformer domain-independent for all post operations via IDomainSpecificOperationProvider
- add getConstants() for predicates
- remove confusing field (fixes #184)
- use SmtSortUtils throughout Ultimate (closes #152)
- try to avoid any INFO logging before the controller takes over
- add Library-InteractiveModel to ultimate common features
- extend TransformedIcfgBuilder s.t. it can also be used to add new transformulas to the icfg (not only transform existing ones)
- refactoring: support several interactive modules in PMaxSAT solver - added new interface for interactive module - former TransitivityGeneralMaxSatSolver became InteractiveMaxSatSolver which supports several modules
- various refactorings in CEGAR loops (towards error automaton, see #182)
Known Issues
README and Website usage instructions still outdated (see #135)