Update various Java examples

Use `java_assert_eq` instead of `java_assert`.

Add an example of returning an array with `java_symexec`.

Fixes #68 (or shows that it's been fixed).

Author: Aaron Tomb

examples/java/arrayfield.saw

@@ -1,7 +1,7 @@
 let init_spec = do {
   a <- java_var "this.a" (java_array 5 java_int);
   x <- java_var "x" java_int;
-  java_assert {{ x == 22 }};
+  java_assert_eq "x" {{ 22 : [32] }};
   java_ensure_eq "this.a" {{ [x, x, x, x, x] }};
   java_allow_alloc;
   java_verify_tactic abc;

examples/java/branchsat.saw

@@ -1,6 +1,6 @@
 let f_spec = do {
    x <- java_var "x" java_int;
-   java_assert {{ x == (4:[32]) }};
+   java_assert_eq "x" {{ 4:[32] }};
    java_sat_branches true;
    java_return {{ 6 : [32] }};
    java_verify_tactic abc;

examples/java/java_add.saw

@@ -2,13 +2,13 @@ let setup (add : Term) : JavaSetup () = do {
     x <- java_var "x" java_int;
     y <- java_var "y" java_int;
     java_return {{ add x y }};
-    java_verify_tactic (do { unfolding ["add"]; yices; });
+    java_verify_tactic (do { unfolding ["add"]; z3; });
 };
 
 let setup' (add : Term) : JavaSetup () = do {
     x <- java_var "x" java_int;
     java_return {{ add x x }};
-    java_verify_tactic yices;
+    java_verify_tactic z3;
 };
 
 let main : TopLevel () = do {

examples/java/return.saw

@@ -1,7 +1,7 @@
 let fill_spec = do {
   x <- java_var "n" java_int;
   java_var "return" (java_array 5 java_int);
-  java_assert {{ x == 22 }};
+  java_assert_eq "n" {{ 22 : [32] }};
   java_ensure_eq "return" {{ [x, x, x, x, x] }};
   // This also works, and means the same thing.
   // java_return {{ [x, x, x, x, x] }};
@@ -15,8 +15,8 @@ let newSimple_spec = do {
   java_class_var "return" (java_class "SimpleObj");
   java_var "return.x" java_int;
   java_var "return.y" java_int;
-  java_assert {{ x == 43 }};
-  java_assert {{ y == 77 }};
+  java_assert_eq "x" {{ 43 : [32] }};
+  java_assert_eq "y" {{ 77 : [32] }};
   java_ensure_eq "return.x" {{ x }};
   java_ensure_eq "return.y" {{ y }};
   java_allow_alloc;
@@ -27,8 +27,8 @@ let simpleWrap2_spec = do {
   java_requires_class "SimpleObj";
   x <- java_var "x" java_int;
   y <- java_var "y" java_int;
-  java_assert {{ x == 43 }};
-  java_assert {{ y == 77 }};
+  java_assert_eq "x" {{ 43 : [32] }};
+  java_assert_eq "y" {{ 77 : [32] }};
   java_return {{ 2 : [32] }};
   java_allow_alloc;
   java_verify_tactic abc;

examples/java/returnsym.saw

@@ -0,0 +1,3 @@
+c <- java_load_class "Return";
+t <- java_symexec c "fill" [("n", {{ 22:[32] }})] ["return"] false;
+print_term t;