From ecd9825a14e90c06e61e3a00ccc83e7a6f0fd125 Mon Sep 17 00:00:00 2001
From: zapashcanon <leo@ndrs.fr>
Date: Mon, 3 Jun 2024 16:46:29 +0200
Subject: [PATCH] add test for immediately failing concolic test

---
 test/conc/dune                 | 2 ++
 test/conc/immediately_fail.t   | 7 +++++++
 test/conc/immediately_fail.wat | 6 ++++++
 3 files changed, 15 insertions(+)
 create mode 100644 test/conc/dune
 create mode 100644 test/conc/immediately_fail.t
 create mode 100644 test/conc/immediately_fail.wat

diff --git a/test/conc/dune b/test/conc/dune
new file mode 100644
index 000000000..b605fece9
--- /dev/null
+++ b/test/conc/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps %{bin:owi} immediately_fail.wat))
diff --git a/test/conc/immediately_fail.t b/test/conc/immediately_fail.t
new file mode 100644
index 000000000..c9f97a89c
--- /dev/null
+++ b/test/conc/immediately_fail.t
@@ -0,0 +1,7 @@
+  $ owi conc immediately_fail.wat
+  Assert failure
+  Model:
+    (model
+      )
+  Reached problem!
+  [13]
diff --git a/test/conc/immediately_fail.wat b/test/conc/immediately_fail.wat
new file mode 100644
index 000000000..2cb09ddf4
--- /dev/null
+++ b/test/conc/immediately_fail.wat
@@ -0,0 +1,6 @@
+(module
+  (import "symbolic" "assert" (func $assert (param i32)))
+  (func $f
+    (i32.const 0)
+    (call $assert))
+  (start $f))