Updated examples.

394797ca · David Hauzar · 9b6d889c · 394797ca
Commit 394797ca authored Apr 13, 2015 by David Hauzar
Hide whitespace changes
Inline Side-by-side

Showing with 7 additions and 1 deletion

examples/tests/cvc4-models.mlw examples/tests/cvc4-models.mlw +7 -1

No files found.
--- a/examples/tests/cvc4-models.mlw
+++ b/examples/tests/cvc4-models.mlw
@@ -4,7 +4,13 @@ module M

  use import int.Int

-  val y "model" "model_trace:y" :ref int
+  function projf (l : int) : int
+  =
+  l+100
+
+  meta "model_projection" function projf
+
+  val y "model" "model_projected" "model_trace:y" :ref int

  let incr ( x "model" "model_trace:x" : ref int ): unit
  ensures { !x = old !x + 2 + !y }