Add boolean tests and update existing tests

example/c/README.md

@@ -35,7 +35,7 @@ $ owi c ./poly.c -w1
 ...
 Model:
   (model
-    (symbol_0 (i32 4)))
+    (symbol_0 0x00000004))
 Reached problem!
 [13]
 ```
@@ -81,7 +81,7 @@ $ owi c ./poly2.c
 ...
 Model:
   (model
-    (symbol_0 (i32 -2147483644)))
+    (symbol_0 0x80000004))
 Reached problem!
 [13]
 ```

example/conc/README.md

@@ -28,7 +28,7 @@ $ owi conc ./mini.wat
 Trap: unreachable
 Model:
   (model
-    (symbol_1 (i32 6)))
+    (symbol_1 0x00000006))
 Reached problem!
 [13]
 ```

example/sym/README.md

@@ -28,7 +28,7 @@ $ owi sym ./mini.wat
 Trap: unreachable
 Model:
   (model
-    (symbol_0 (i32 6)))
+    (symbol_0 0x00000006))
 Reached problem!
 [13]
 ```

test/c/bool.c

@@ -0,0 +1,9 @@
+#include <owi.h>
+
+int main() {
+    _Bool b1 = owi_bool(), b2 = owi_bool();
+    owi_assume(b1 || b2);
+    owi_assume(b1 || !b2);
+    owi_assert(b1);
+    return 0;
+}

test/c/bool.t

@@ -0,0 +1,2 @@
+  $ owi c ./bool.c
+  All OK

test/c/collections-c/array_tests.t

@@ -29,10 +29,10 @@ Array tests:
   Assert failure: (bool.ne symbol_3 symbol_2)
   Model:
     (model
-      (symbol_0 (i32 0))
-      (symbol_1 (i32 0))
-      (symbol_2 (i32 0))
-      (symbol_3 (i32 0)))
+      (symbol_0 0x00000000)
+      (symbol_1 0x00000000)
+      (symbol_2 0x00000000)
+      (symbol_3 0x00000000))
   Reached problem!
   [13]
   $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_reverse.c

test/c/collections-c/buggy_tests.t

@@ -3,7 +3,7 @@ Bug-triggering tests:
   Trap: memory heap buffer overflow
   Model:
     (model
-      (symbol_0 (i32 8)))
+      (symbol_0 0x00000008))
   Reached problem!
   [13]
   $ owi c -I files/bugs/include files/bugs/src/list.c files/bugs/src/common.c files/bugs/src/utils.c files/bugs/testsuite/list_test_zipIterAdd.c --no-value

test/c/dune

@@ -2,6 +2,7 @@
  (deps
   %{bin:owi}
   (package owi)
+  bool.c
+  exit.c
   malloc_aligned.c
-  main.c
-  exit.c))
+  main.c))

test/c/test-comp/simple.t

@@ -1,7 +1,7 @@
   $ owi c -O0 --testcomp ./simple.c
-  Assert failure: (bool.ne (i32.mul symbol_0 symbol_0) (i32 0))
+  Assert failure: (bool.ne (i32.mul symbol_0 symbol_0) 0x00000000)
   Model:
     (model
-      (symbol_0 (i32 0)))
+      (symbol_0 0x00000000))
   Reached problem!
   [13]

test/sym/add.t

@@ -1,14 +1,14 @@
 add binop:
   $ owi sym add_i32.wat --no-value --deterministic-result-order
-  Assert failure: (i32.le (i32 0) (i32.add symbol_0 symbol_1))
+  Assert failure: (i32.le 0x00000000 (i32.add symbol_0 symbol_1))
   Model:
     (model
       (symbol_0 i32)
       (symbol_1 i32))
   Reached problem!
   [13]
   $ owi sym add_i64.wat --no-value --deterministic-result-order
-  Assert failure: (i64.le (i64 0) (i64.add symbol_0 symbol_1))
+  Assert failure: (i64.le 0x0000000000000000 (i64.add symbol_0 symbol_1))
   Model:
     (model
       (symbol_0 i64)

test/sym/binop/f32/f32_binop.t

@@ -27,14 +27,14 @@ f32:
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (f32 1.)))
+      (symbol_0 (fp 0x3f800000)))
   Reached problem!
   [13]
   $ owi sym f32_ge.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (f32 1.)))
+      (symbol_0 (fp 0x3f800000)))
   Reached problem!
   [13]
   $ owi sym f32_gt.wat --no-stop-at-failure --no-value
@@ -48,7 +48,7 @@ f32:
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (f32 1.)))
+      (symbol_0 (fp 0x3f800000)))
   Reached problem!
   [13]
   $ owi sym f32_lt.wat --no-stop-at-failure --no-value

test/sym/binop/f64/f64_binop.t

@@ -27,28 +27,28 @@ f64:
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (f64 1.)))
+      (symbol_0 (fp 0x3ff0000000000000)))
   Reached problem!
   [13]
   $ owi sym f64_ge.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (f64 1.)))
+      (symbol_0 (fp 0x3ff0000000000000)))
   Reached problem!
   [13]
   $ owi sym f64_gt.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (f64 2.)))
+      (symbol_0 (fp 0x4000000000000001)))
   Reached problem!
   [13]
   $ owi sym f64_le.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (f64 1.)))
+      (symbol_0 (fp 0x3ff0000000000000)))
   Reached problem!
   [13]
   $ owi sym f64_lt.wat --no-stop-at-failure --no-value

test/sym/binop/i32/i32_binop.t

@@ -3,7 +3,7 @@ i32:
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 -1)))
+      (symbol_0 0xffffffff))
   Reached problem!
   [13]
   $ owi sym i32_and.wat --no-stop-at-failure --no-value
@@ -18,147 +18,147 @@ i32:
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0)))
+      (symbol_0 0x00000000))
   Reached problem!
   [13]
   $ owi sym i32_div_u.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0)))
+      (symbol_0 0x00000000))
   Reached problem!
   [13]
   $ owi sym i32_eq.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 1)))
+      (symbol_0 0x00000001))
   Reached problem!
   [13]
   $ owi sym i32_ge_s.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 1073741824)))
+      (symbol_0 0x40000000))
   Reached problem!
   [13]
   $ owi sym i32_gt_s.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 2)))
+      (symbol_0 0x00000002))
   Reached problem!
   [13]
   $ owi sym i32_le_s.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 -2147483646)))
+      (symbol_0 0x80000002))
   Reached problem!
   [13]
   $ owi sym i32_lt_s.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0)))
+      (symbol_0 0x00000000))
   Reached problem!
   [13]
   $ owi sym i32_mul.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0)))
+      (symbol_0 0x00000000))
   Reached problem!
   [13]
   $ owi sym i32_ne.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0)))
+      (symbol_0 0x00000000))
   Reached problem!
   [13]
   $ owi sym i32_or.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 1))
-      (symbol_1 (i32 0)))
+      (symbol_0 0x00000001)
+      (symbol_1 0x00000000))
   Reached problem!
   [13]
   $ owi sym i32_rem_s.wat --no-stop-at-failure --deterministic-result-order
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 -1)))
+      (symbol_0 0xffffffff))
   Trap: integer divide by zero
   Model:
     (model
-      (symbol_0 (i32 0)))
+      (symbol_0 0x00000000))
   Reached 2 problems!
   [13]
   $ owi sym i32_rem_u.wat --no-stop-at-failure --deterministic-result-order
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 1)))
+      (symbol_0 0x00000001))
   Trap: integer divide by zero
   Model:
     (model
-      (symbol_0 (i32 0)))
+      (symbol_0 0x00000000))
   Reached 2 problems!
   [13]
   $ owi sym i32_rotl.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0))
-      (symbol_1 (i32 0)))
+      (symbol_0 0x00000000)
+      (symbol_1 0x00000000))
   Reached problem!
   [13]
   $ owi sym i32_rotr.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0))
-      (symbol_1 (i32 0)))
+      (symbol_0 0x00000000)
+      (symbol_1 0x00000000))
   Reached problem!
   [13]
   $ owi sym i32_shl.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0))
-      (symbol_1 (i32 0)))
+      (symbol_0 0x00000000)
+      (symbol_1 0x00000000))
   Reached problem!
   [13]
   $ owi sym i32_shr_s.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0))
-      (symbol_1 (i32 0)))
+      (symbol_0 0x00000000)
+      (symbol_1 0x00000000))
   Reached problem!
   [13]
   $ owi sym i32_shr_u.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0))
-      (symbol_1 (i32 0)))
+      (symbol_0 0x00000000)
+      (symbol_1 0x00000000))
   Reached problem!
   [13]
   $ owi sym i32_sub.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 1)))
+      (symbol_0 0x00000001))
   Reached problem!
   [13]
   $ owi sym i32_xor.wat --no-stop-at-failure
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 -67108865))
-      (symbol_1 (i32 67108864)))
+      (symbol_0 0xfbffffff)
+      (symbol_1 0x04000000))
   Reached problem!
   [13]