• Sylvain Dailler's avatar
    P530-020 counterex - Disallow printing of value not introduced · 76c67c9c
    Sylvain Dailler authored
    I introduced bug with last counterexample commit. This was due to
    querying counterexample value of variables that were not introduced. This
    commits introduce a container that save introduced variables and check if
    they should be taken as counterex.
    * src/transform/intro_vc_vars_counterexmp.ml
    (do_intro): Adding vc_var which contains all variables that we can safely
    print as counterexamples.
    (remove_positive_foralls): Adding vc_var and introduce variables in vc_var
    when quantified over.
    (intros): Adding vc_var.
    (do_intro_vc_vars_counterexmp): Adding vc_var.
    Change-Id: Ic6bf732f1e50241a42df8e097f52aa46dd473bd2
intro_vc_vars_counterexmp.ml 13.6 KB