never encode enums and records for Alt-Ergo

[why3.git] / drivers / cvc4_17_counterexample.drv

prelude ";; produced by cvc4_17_counterexample.drv ;;"

import "cvc4_17.drv"

(* Counterexamples: set model parser *)
model_parser "smtv2"

theory BuiltIn

  meta "get_counterexmp" ""
  meta "meta_incremental" ""

end