drivers/alt_ergo_counterexamples.drv

   1
   2 prelude ";; produced by alt_ergo_counterexample.drv ;;"
   3
   4 import "alt_ergo_smt.drv"
   5
   6 (* Prepare for counter-example query: get rid of some quantifiers
   7    (makes it possible to query model values of the variables in
   8    premises) and introduce counter-example projections.  Note: does
   9    nothing if meta get_counterexmp is not set *)
  10 transformation "prepare_for_counterexmp"
  11
  12 (* Counterexamples: set model parser *)
  13 model_parser "smtv2"
  14
  15 theory BuiltIn
  16
  17   meta "get_counterexmp" ""
  18   meta "meta_incremental" ""
  19
  20 end