• MARCHE Claude's avatar
    New setting for counterexample generation · eaba8837
    MARCHE Claude authored
    - no option -get-ce and option in IDE anymore
    
      instead counterexamples are generated using prover alternatives
    
    - for counterexamples, smt printer always prints incrementally: first the goal,
      then the ground hypotheses, then the others
    eaba8837
z3_440_counterexample.drv 100 Bytes