alt_ergo_0.93.drv 343 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
import "alt_ergo_bare.drv"

theory BuiltIn
  meta "eliminate_algebraic" "keep_enums"
end

theory map.Map
  syntax type  map "(%1,%2) farray"

  syntax function get "(%1[%2])"
  syntax function set "(%1[%2 <- %3])"

  remove prop Select_eq
  remove prop Select_neq
end

(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)