• Sylvain Dailler's avatar
    ce: support for if-branching · b0ef7adf
    Sylvain Dailler authored
    This adds introduce_premises as a counterexample transformation (to
    introduce possible exists quantifications) and add attributes that are
    tagged with the special branch_id= to variables directly near it.
    b0ef7adf
cntexmp_printer.ml 5.1 KB