diff --git a/test/sym/add.t b/test/sym/add.t
new file mode 100644
index 000000000..04359e13e
--- /dev/null
+++ b/test/sym/add.t
@@ -0,0 +1,15 @@
+add binop:
+  $ dune exec owi -- sym add_i32.wat
+  Assert failure: (i32.le (i32 0) (i32.add symbol_0 symbol_1))
+  Model:
+    (model
+      (symbol_0 (i32 1073741825))
+      (symbol_1 (i32 1073741824)))
+  Reached problem!
+  $ dune exec owi -- sym add_i64.wat
+  Assert failure: (i64.le (i64 0) (i64.add symbol_0 symbol_1))
+  Model:
+    (model
+      (symbol_0 (i64 4611686018427387905))
+      (symbol_1 (i64 4611686018427387904)))
+  Reached problem!
diff --git a/test/sym/add_i32.wat b/test/sym/add_i32.wat
new file mode 100644
index 000000000..d65d5e29c
--- /dev/null
+++ b/test/sym/add_i32.wat
@@ -0,0 +1,20 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "assume_positive_i32" (func $assume_positive_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i32)
+    (local $y i32)
+
+    (local.set $x (call $i32_symbol))
+    (local.set $y (call $i32_symbol))
+
+    (call $assume_positive_i32 (local.get $x))  ;; x >= 0
+    (call $assume_positive_i32 (local.get $y))  ;; y >= 0
+    (call $assert_i32                           ;; x + y >= 0 (== 0 =< x + y)
+      (i32.le_s (i32.const 0) (i32.add (local.get $x) (local.get $y))))
+  )
+
+  (start $start)
+)
diff --git a/test/sym/add_i64.wat b/test/sym/add_i64.wat
new file mode 100644
index 000000000..b448a091d
--- /dev/null
+++ b/test/sym/add_i64.wat
@@ -0,0 +1,22 @@
+(module
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+  (import "symbolic" "assume" (func $assume_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i64)
+    (local $y i64)
+
+    (local.set $x (call $i64_symbol))
+    (local.set $y (call $i64_symbol))
+
+    (call $assume_i32
+      (i64.ge_s (local.get $x) (i64.const 0)))    ;; x >= 0
+    (call $assume_i32
+      (i64.ge_s (local.get $y) (i64.const 0)))    ;; y >= 0
+    (call $assert_i32                             ;; x + y >= 0 (== 0 =< x + y)
+      (i64.le_s (i64.const 0) (i64.add (local.get $x) (local.get $y))))
+  )
+
+  (start $start)
+)
diff --git a/test/sym/div.t b/test/sym/div.t
new file mode 100644
index 000000000..988a18e37
--- /dev/null
+++ b/test/sym/div.t
@@ -0,0 +1,15 @@
+div binop:
+  $ dune exec owi -- sym div_i32.wat
+  Trap: integer overflow
+  Model:
+    (model
+      (symbol_0 (i32 -2147483648))
+      (symbol_1 (i32 -1)))
+  Reached problem!
+  $ dune exec owi -- sym div_i64.wat
+  Trap: integer overflow
+  Model:
+    (model
+      (symbol_0 (i64 -9223372036854775808))
+      (symbol_1 (i64 -1)))
+  Reached problem!
diff --git a/test/sym/div_i32.wat b/test/sym/div_i32.wat
new file mode 100644
index 000000000..e7d7c048d
--- /dev/null
+++ b/test/sym/div_i32.wat
@@ -0,0 +1,19 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+
+  (func $start
+
+    (local $x i32)
+    (local $y i32)
+
+    (local.set $x (call $i32_symbol))
+    (local.set $y (call $i32_symbol))
+
+    local.get $x
+    local.get $y
+    i32.div_s     ;; MIN_INT/(-1) != MAX_INT -- MAX_INT = (-MIN_INT)-1
+    drop
+  )
+
+  (start $start)
+)
diff --git a/test/sym/div_i64.wat b/test/sym/div_i64.wat
new file mode 100644
index 000000000..54c293db4
--- /dev/null
+++ b/test/sym/div_i64.wat
@@ -0,0 +1,19 @@
+(module
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+
+  (func $start
+
+    (local $x i64)
+    (local $y i64)
+
+    (local.set $x (call $i64_symbol))
+    (local.set $y (call $i64_symbol))
+
+    local.get $x
+    local.get $y
+    i64.div_s     ;; MIN_INT/(-1) != MAX_INT -- MAX_INT = (-MIN_INT)-1
+    drop
+  )
+
+  (start $start)
+)
diff --git a/test/sym/dune b/test/sym/dune
index 47203cefd..841242924 100644
--- a/test/sym/dune
+++ b/test/sym/dune
@@ -1,19 +1,28 @@
 (cram
  (deps
   %{bin:owi}
-  mini_test.wat
+  add_i32.wat
+  add_i64.wat
   assume.wat
-  binop_i32.wat
-  binop_i32-2.wat
-  binop_i64.wat
-  binop_i64-2.wat
-  binop_f32.wat
-  binop_f64.wat
-  global.wat
-  grow.wat
-  memory.wat
+  ; binop_i32.wat
+  ; binop_i32-2.wat
+  ; binop_i64.wat
+  ; binop_i64-2.wat
+  ; binop_f32.wat
+  ; binop_f64.wat
+  div_i32.wat
+  div_i64.wat
+  ; global.wat
+  ; grow.wat
+  ; memory.wat
+  mini_test.wat
+  mul_i32.wat
+  mul_i64.wat
+  sub_i32.wat
+  sub_i64.wat
   table.wat
-  unop_i32.wat
-  unop_i64.wat
-  unop_f32.wat
-  unop_f64.wat))
+  ; unop_i32.wat
+  ; unop_i64.wat
+  ; unop_f32.wat
+  ; unop_f64.wat
+ ))
diff --git a/test/sym/mul.t b/test/sym/mul.t
new file mode 100644
index 000000000..b133662ed
--- /dev/null
+++ b/test/sym/mul.t
@@ -0,0 +1,15 @@
+mul binop:
+  $ dune exec owi -- sym mul_i32.wat
+  Assert failure: (i32.ge (i32.mul symbol_0 symbol_1) (i32 0))
+  Model:
+    (model
+      (symbol_0 (i32 792711941))
+      (symbol_1 (i32 229807418)))
+  Reached problem!
+  $ dune exec owi -- sym mul_i64.wat
+  Assert failure: (i64.ge (i64.mul symbol_0 symbol_1) (i64 0))
+  Model:
+    (model
+      (symbol_0 (i64 3276315702285119495))
+      (symbol_1 (i64 4152879772057883690)))
+  Reached problem!
diff --git a/test/sym/mul_i32.wat b/test/sym/mul_i32.wat
new file mode 100644
index 000000000..20cdd1e7e
--- /dev/null
+++ b/test/sym/mul_i32.wat
@@ -0,0 +1,20 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "assume_positive_i32" (func $assume_positive_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i32)
+    (local $y i32)
+
+    (local.set $x (call $i32_symbol))
+    (local.set $y (call $i32_symbol))
+
+    (call $assume_positive_i32 (local.get $x))  ;; x >= 0
+    (call $assume_positive_i32 (local.get $y))  ;; y >= 0
+    (call $assert_i32                           ;; x * y >= 0
+      (i32.ge_s (i32.mul (local.get $x) (local.get $y)) (i32.const 0)))
+  )
+
+  (start $start)
+)
diff --git a/test/sym/mul_i64.wat b/test/sym/mul_i64.wat
new file mode 100644
index 000000000..3577e6c09
--- /dev/null
+++ b/test/sym/mul_i64.wat
@@ -0,0 +1,22 @@
+(module
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+  (import "symbolic" "assume" (func $assume_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i64)
+    (local $y i64)
+
+    (local.set $x (call $i64_symbol))
+    (local.set $y (call $i64_symbol))
+
+    (call $assume_i32
+      (i64.ge_s (local.get $x) (i64.const 0)))  ;; y >= 0
+    (call $assume_i32
+      (i64.ge_s (local.get $y) (i64.const 0)))  ;; y >= 0
+    (call $assert_i32                           ;; x * y >= 0
+      (i64.ge_s (i64.mul (local.get $x) (local.get $y)) (i64.const 0)))
+  )
+
+  (start $start)
+)
diff --git a/test/sym/sub.t b/test/sym/sub.t
new file mode 100644
index 000000000..867c5c982
--- /dev/null
+++ b/test/sym/sub.t
@@ -0,0 +1,15 @@
+sub binop:
+  $ dune exec owi -- sym sub_i32.wat
+  Assert failure: (i32.ge symbol_0 (i32.sub symbol_0 symbol_1))
+  Model:
+    (model
+      (symbol_0 (i32 -2147483648))
+      (symbol_1 (i32 2147483645)))
+  Reached problem!
+  $ dune exec owi -- sym sub_i64.wat
+  Assert failure: (i64.ge symbol_0 (i64.sub symbol_0 symbol_1))
+  Model:
+    (model
+      (symbol_0 (i64 -9223372036854775808))
+      (symbol_1 (i64 9223372036854775805)))
+  Reached problem!
diff --git a/test/sym/sub_i32.wat b/test/sym/sub_i32.wat
new file mode 100644
index 000000000..7e60126bb
--- /dev/null
+++ b/test/sym/sub_i32.wat
@@ -0,0 +1,19 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "assume_positive_i32" (func $assume_positive_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i32)
+    (local $y i32)
+
+    (local.set $x (call $i32_symbol))
+    (local.set $y (call $i32_symbol))
+
+    (call $assume_positive_i32 (local.get $y))  ;; y >= 0
+    (call $assert_i32                           ;; x >= x - y
+      (i32.ge_s (local.get $x) (i32.sub (local.get $x) (local.get $y))))
+  )
+
+  (start $start)
+)
diff --git a/test/sym/sub_i64.wat b/test/sym/sub_i64.wat
new file mode 100644
index 000000000..8a6c420a2
--- /dev/null
+++ b/test/sym/sub_i64.wat
@@ -0,0 +1,20 @@
+(module
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+  (import "symbolic" "assume" (func $assume_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i64)
+    (local $y i64)
+
+    (local.set $x (call $i64_symbol))
+    (local.set $y (call $i64_symbol))
+
+    (call $assume_i32
+      (i64.ge_s (local.get $y) (i64.const 0)))  ;; y >= 0
+    (call $assert_i32                           ;; x >= x - y
+      (i64.ge_s (local.get $x) (i64.sub (local.get $x) (local.get $y))))
+  )
+
+  (start $start)
+)