Fixed JSON output for unknown realizability results

v2.2

Fixed handling of unknown results when printing in json format.

Example traces for realizable results

• An example execution trace is now computed for realizable contracts, when using the fixpoint option and Z3 as the main solver.
• An option -tracelength X has been added, to allow users to designate the length of the computed example trace from above. Automatically enables the -fixpoint option.

Added option to switch between QE algorithms when using AE-VAL

v2.0

Added option to switch between QE algorithms when using AE-VAL.

Updated QE tactics for realizability checking

Added additional QE tactics to improve performance for fixpoint algorithm.

Latest binary

New fixpoint implementation for realizability checking based on Z3 quantifier elimination tactics. Many thanks to Daniel Larraz and Stanly Samuel for the fruitful discussions.

Fixed bug regarding capturing all inclusive skolems from AE-VAL

JSYN1.7

Fixed bug on recognizing realizability inputs and outputs

Various fixes

Re-enabled consistency check for fixpoint engine and fixed bugs.

Added support for nondeterministic synthesis

Added option to enable nondeterministic synthesis, as well as options for compact and all-inclusive solutions.

Added region simplification procedure

JSYNv1.4.1

Added simplification procedure to reduce size of synthesized implemen…

Minor bug fixes

• Inclusion of assumptions to pre-input variables
• Minor code cleanup
• Inclusion of experimental option fixpoint_T