From e6b2349485f5d002b7c2c054054db99bc3f79cc6 Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Wed, 10 Sep 2025 17:09:32 +0200
Subject: [PATCH 01/13] Add a series of tests for the concolic execution engine

---
 build.gradle.kts                              |   2 +-
 .../be/ugent/topl/mio/concolic/Analyse.kt     |  37 +++-
 src/test/kotlin/concolic/ConcolicTests.kt     | 194 ++++++++++++++++++
 3 files changed, 225 insertions(+), 8 deletions(-)
 create mode 100644 src/test/kotlin/concolic/ConcolicTests.kt

diff --git a/build.gradle.kts b/build.gradle.kts
index 4fcc748..2db4e33 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -1,7 +1,7 @@
 import java.util.*
 
 plugins {
-    kotlin("jvm") version "2.0.0"
+    kotlin("jvm") version "2.2.0"
     application
 }
 
diff --git a/src/main/kotlin/be/ugent/topl/mio/concolic/Analyse.kt b/src/main/kotlin/be/ugent/topl/mio/concolic/Analyse.kt
index 80e461d..d0234c3 100644
--- a/src/main/kotlin/be/ugent/topl/mio/concolic/Analyse.kt
+++ b/src/main/kotlin/be/ugent/topl/mio/concolic/Analyse.kt
@@ -14,16 +14,36 @@ data class SymbolicValueMapping(val primitive: String, val arg: Int, val value:
     }
 }
 
-data class ConcolicAnalysisResult(val paths: List<SymbolicValueMapping>)
+data class ConcolicAnalysisResult(val paths: List<SymbolicValueMapping>) {
+    fun getPathCount(): Int {
+        return getPathCount(paths)
+    }
+    private fun getPathCount(paths: List<SymbolicValueMapping>): Int {
+        if (paths.isEmpty()) {
+            return 1
+        }
+
+        var count = 0
+        for (path in paths) {
+            count += getPathCount(path.paths)
+        }
+        return count
+    }
+}
 
-fun analyse(wdcliPath: String, wasmFile: String, jsonSnapshot: String, maxInstructions: Int = 50, maxSymbolicVariables: Int = -1, maxIterations: Int = -1, stopPc: Int = -1): ConcolicAnalysisResult {
-    val woodState = WOODState.fromLine(jsonSnapshot)
-    val messages = woodState.toBinary(io = false, overrides = false).map { it.trim('\n', ' ') }
-    for (msg in messages) {
-        println("\"$msg\"")
+fun analyse(wdcliPath: String, wasmFile: String, jsonSnapshot: String?, maxInstructions: Int = 50, maxSymbolicVariables: Int = -1, maxIterations: Int = -1, stopPc: Int = -1): ConcolicAnalysisResult {
+    val command = if (jsonSnapshot != null) {
+        val woodState = WOODState.fromLine(jsonSnapshot)
+        val messages = woodState.toBinary(io = false, overrides = false).map { it.trim('\n', ' ') }
+        for (msg in messages) {
+            println("\"$msg\"")
+        }
+        listOf(wdcliPath, wasmFile, "--no-socket", "--mode", "concolic", "--snapshot", *messages.toTypedArray(), "end", "--max-instructions", "$maxInstructions", "--max-symbolic-variables", "$maxSymbolicVariables", "--max-iterations", "$maxIterations", "--stop-at-pc", "$stopPc")
+    }
+    else {
+        listOf(wdcliPath, wasmFile, "--no-socket", "--mode", "concolic", "--max-instructions", "$maxInstructions", "--max-symbolic-variables", "$maxSymbolicVariables", "--max-iterations", "$maxIterations", "--stop-at-pc", "$stopPc")
     }
 
-    val command = listOf(wdcliPath, wasmFile, "--no-socket", "--mode", "concolic", "--snapshot", *messages.toTypedArray(), "end", "--max-instructions", "$maxInstructions", "--max-symbolic-variables", "$maxSymbolicVariables", "--max-iterations", "$maxIterations", "--stop-at-pc", "$stopPc")
     println("Running command: ${command.joinToString(" ") }")
     val process = ProcessBuilder(command).redirectErrorStream(true).start()
     val lineScanner = Scanner(process.inputStream)
@@ -40,6 +60,9 @@ fun analyse(wdcliPath: String, wasmFile: String, jsonSnapshot: String, maxInstru
             //process(result)
             return ConcolicAnalysisResult(result.paths.sortedBy { it.value })
         }
+        if (currentLine.startsWith("Trap:")) {
+            throw Exception("Execution resulted in a trap!")
+        }
     }
     process.destroy()
     println("Output:")
diff --git a/src/test/kotlin/concolic/ConcolicTests.kt b/src/test/kotlin/concolic/ConcolicTests.kt
new file mode 100644
index 0000000..675eb30
--- /dev/null
+++ b/src/test/kotlin/concolic/ConcolicTests.kt
@@ -0,0 +1,194 @@
+package concolic
+
+import DebuggerTestBase
+import be.ugent.topl.mio.concolic.ConcolicAnalysisResult
+import be.ugent.topl.mio.concolic.analyse
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.ValueSource
+import java.io.File
+import kotlin.test.assertEquals
+
+class ConcolicTests : DebuggerTestBase() {
+    @Test
+    fun `Test result without any branches`() {
+        val wasmFile = getFile("blink.wasm").absolutePath
+        val result = analyse(config.symbolicWdcliPath, wasmFile, null, maxInstructions = 100)
+        assertEquals(listOf(),result.paths)
+    }
+
+    private fun makeWat(content: String): String {
+        return "(module\n" +
+                "(import \"env\" \"chip_analog_read\" (func \$chip_analog_read (param i32) (result i32)))\n" +
+                "(func \$main (local i32)\n" +
+                content +
+                ")\n(export \"main\" (func \$main)))"
+    }
+
+    fun getPathsFromWat(watString: String): ConcolicAnalysisResult {
+        File("temp.wat").writeText(watString)
+        val exitCode = ProcessBuilder("wat2wasm", "temp.wat").inheritIO().start().waitFor()
+        if (exitCode != 0) {
+            throw IllegalStateException("Could not compile wat")
+        }
+        return analyse(config.symbolicWdcliPath, "temp.wasm", null, maxInstructions = 200)
+    }
+
+    @Test
+    fun `Test wat`() {
+        val watString = makeWat("""
+            i32.const 3
+            i32.const 1
+            i32.add
+            drop
+        """.trimIndent())
+        val result = getPathsFromWat(watString)
+        assertEquals(listOf(),result.paths)
+    }
+
+    @Test
+    fun `Test wat if 2 paths`() {
+        val watString = makeWat($$"""
+            i32.const 0
+            call $chip_analog_read
+            i32.const 10
+            i32.lt_s
+            if
+                nop
+            end
+        """.trimIndent())
+        val result = getPathsFromWat(watString)
+        assertEquals(2,result.paths.size)
+    }
+
+    @Test
+    fun `Test wat if 3 paths`() {
+        val watString = makeWat($$"""
+            i32.const 0
+            call $chip_analog_read
+            local.tee 0
+            i32.const 10
+            i32.lt_s
+            if
+                nop
+            else
+                local.get 0
+                i32.const 20
+                i32.lt_s
+                if
+                    nop
+                end
+            end
+        """.trimIndent())
+        val result = getPathsFromWat(watString)
+        assertEquals(3,result.paths.size)
+    }
+
+    @ParameterizedTest(name = "{0} loop iteration(s)")
+    @ValueSource(ints = [1, 2, 3, 4, 5, 6, 7])
+    fun testIfLoop(iterations: Int = 2) {
+        val watString = makeWat($$"""
+            (loop $for_2
+                i32.const 0
+                call $chip_analog_read
+                i32.const 10
+                i32.lt_s
+                if
+                    nop
+                end
+            
+                local.get 0
+                i32.const 1
+                i32.add
+                local.tee 0
+                i32.const $${iterations}
+                i32.lt_s
+                br_if $for_2)
+        """.trimIndent())
+        val result = getPathsFromWat(watString)
+        println(result)
+        val expectedIterationCount = 1 shl iterations
+        println("Expect $expectedIterationCount paths for $iterations iteration(s)")
+        assertEquals(expectedIterationCount,result.getPathCount())
+    }
+
+    @Test
+    fun `Test wat floats no branches`() {
+        val watString = makeWat($$"""
+            f32.const 0.0
+            f32.const 5.0
+            f32.add
+            drop
+        """.trimIndent())
+        val result = getPathsFromWat(watString)
+        assertEquals(1,result.getPathCount())
+    }
+
+    @Test
+    fun `Test wat floats equal`() {
+        val watString = makeWat($$"""
+            i32.const 0
+            call $chip_analog_read
+            f32.convert_i32_s
+            f32.const 5.0
+            f32.eq
+            if
+                nop
+            end
+        """.trimIndent())
+        val result = getPathsFromWat(watString)
+        assertEquals(2,result.getPathCount())
+    }
+
+    @Test
+    fun `Test wat floats not equal`() {
+        val watString = makeWat($$"""
+            i32.const 0
+            call $chip_analog_read
+            f32.convert_i32_s
+            f32.const 5.0
+            f32.ne
+            if
+                nop
+            end
+        """.trimIndent())
+        val result = getPathsFromWat(watString)
+        assertEquals(2,result.getPathCount())
+    }
+
+    @Test
+    fun `Test wat floats less than`() {
+        val watString = makeWat($$"""
+            i32.const 0
+            call $chip_analog_read
+            f32.convert_i32_s
+            f32.const 5.0
+            f32.lt
+            if
+                nop
+            end
+        """.trimIndent())
+        val result = getPathsFromWat(watString)
+        assertEquals(2,result.getPathCount())
+    }
+
+    @Test
+    fun `Test wat floats less than 2`() {
+        val watString = makeWat($$"""
+            i32.const 0
+            call $chip_analog_read
+            f32.convert_i32_s
+            f32.const 3.0
+            f32.mul
+            f32.const 2.0
+            f32.add
+            f32.const 50.0
+            f32.lt
+            if
+                nop
+            end
+        """.trimIndent())
+        val result = getPathsFromWat(watString)
+        assertEquals(2,result.getPathCount())
+    }
+}

From b024308a451329ce27df2b3e7befda63c6937aad Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Thu, 11 Sep 2025 10:25:12 +0200
Subject: [PATCH 02/13] Add tests with float to int conversion instructions

---
 src/test/kotlin/concolic/ConcolicTests.kt | 103 ++++++++++++++++------
 1 file changed, 74 insertions(+), 29 deletions(-)

diff --git a/src/test/kotlin/concolic/ConcolicTests.kt b/src/test/kotlin/concolic/ConcolicTests.kt
index 675eb30..8c27b7d 100644
--- a/src/test/kotlin/concolic/ConcolicTests.kt
+++ b/src/test/kotlin/concolic/ConcolicTests.kt
@@ -3,12 +3,15 @@ package concolic
 import DebuggerTestBase
 import be.ugent.topl.mio.concolic.ConcolicAnalysisResult
 import be.ugent.topl.mio.concolic.analyse
+import org.junit.jupiter.api.DisplayName
+import org.junit.jupiter.api.Nested
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.ValueSource
 import java.io.File
 import kotlin.test.assertEquals
 
+@DisplayName("WARDuino concolic execution tests")
 class ConcolicTests : DebuggerTestBase() {
     @Test
     fun `Test result without any branches`() {
@@ -112,21 +115,24 @@ class ConcolicTests : DebuggerTestBase() {
         assertEquals(expectedIterationCount,result.getPathCount())
     }
 
-    @Test
-    fun `Test wat floats no branches`() {
-        val watString = makeWat($$"""
+    @Nested
+    @DisplayName("Floating point operations")
+    inner class FloatTests {
+        @Test
+        fun `Test wat floats no branches`() {
+            val watString = makeWat($$"""
             f32.const 0.0
             f32.const 5.0
             f32.add
             drop
         """.trimIndent())
-        val result = getPathsFromWat(watString)
-        assertEquals(1,result.getPathCount())
-    }
+            val result = getPathsFromWat(watString)
+            assertEquals(1,result.getPathCount())
+        }
 
-    @Test
-    fun `Test wat floats equal`() {
-        val watString = makeWat($$"""
+        @Test
+        fun `Test wat floats equal`() {
+            val watString = makeWat($$"""
             i32.const 0
             call $chip_analog_read
             f32.convert_i32_s
@@ -136,13 +142,13 @@ class ConcolicTests : DebuggerTestBase() {
                 nop
             end
         """.trimIndent())
-        val result = getPathsFromWat(watString)
-        assertEquals(2,result.getPathCount())
-    }
+            val result = getPathsFromWat(watString)
+            assertEquals(2,result.getPathCount())
+        }
 
-    @Test
-    fun `Test wat floats not equal`() {
-        val watString = makeWat($$"""
+        @Test
+        fun `Test wat floats not equal`() {
+            val watString = makeWat($$"""
             i32.const 0
             call $chip_analog_read
             f32.convert_i32_s
@@ -152,13 +158,13 @@ class ConcolicTests : DebuggerTestBase() {
                 nop
             end
         """.trimIndent())
-        val result = getPathsFromWat(watString)
-        assertEquals(2,result.getPathCount())
-    }
+            val result = getPathsFromWat(watString)
+            assertEquals(2,result.getPathCount())
+        }
 
-    @Test
-    fun `Test wat floats less than`() {
-        val watString = makeWat($$"""
+        @Test
+        fun `Test wat floats less than`() {
+            val watString = makeWat($$"""
             i32.const 0
             call $chip_analog_read
             f32.convert_i32_s
@@ -168,13 +174,13 @@ class ConcolicTests : DebuggerTestBase() {
                 nop
             end
         """.trimIndent())
-        val result = getPathsFromWat(watString)
-        assertEquals(2,result.getPathCount())
-    }
+            val result = getPathsFromWat(watString)
+            assertEquals(2,result.getPathCount())
+        }
 
-    @Test
-    fun `Test wat floats less than 2`() {
-        val watString = makeWat($$"""
+        @Test
+        fun `Test wat floats less than 2`() {
+            val watString = makeWat($$"""
             i32.const 0
             call $chip_analog_read
             f32.convert_i32_s
@@ -188,7 +194,46 @@ class ConcolicTests : DebuggerTestBase() {
                 nop
             end
         """.trimIndent())
-        val result = getPathsFromWat(watString)
-        assertEquals(2,result.getPathCount())
+            val result = getPathsFromWat(watString)
+            assertEquals(2,result.getPathCount())
+        }
+
+        @Test
+        fun `Test wat floats i32_trunc_f32_s basic`() {
+            val watString = makeWat($$"""
+            i32.const 0
+            call $chip_analog_read
+            f32.convert_i32_s
+            i32.trunc_f32_s
+            i32.const 10
+            i32.lt_s
+            if
+                nop
+            end
+        """.trimIndent())
+            val result = getPathsFromWat(watString)
+            assertEquals(2,result.getPathCount())
+        }
+
+        @Test
+        fun `Test wat floats i32_trunc_f32_s advanced`() {
+            val watString = makeWat($$"""
+            i32.const 0
+            call $chip_analog_read
+            f32.convert_i32_s
+            f32.const 0x1.f3b646p-2 (;=0.488;)
+            f32.mul
+            f32.const 0x1.9p+5 (;=50;)
+            f32.sub
+            i32.trunc_f32_s
+            i32.const 50
+            i32.lt_s
+            if
+                nop
+            end
+        """.trimIndent())
+            val result = getPathsFromWat(watString)
+            assertEquals(2,result.getPathCount())
+        }
     }
 }

From 7134b82230ebd352e962ce81f6c153166aea0216 Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Thu, 11 Sep 2025 11:42:14 +0200
Subject: [PATCH 03/13] Add some additional assertions on the values found +
 between test for floats

---
 src/test/kotlin/concolic/ConcolicTests.kt | 39 +++++++++++++++++++++--
 1 file changed, 37 insertions(+), 2 deletions(-)

diff --git a/src/test/kotlin/concolic/ConcolicTests.kt b/src/test/kotlin/concolic/ConcolicTests.kt
index 8c27b7d..c9084df 100644
--- a/src/test/kotlin/concolic/ConcolicTests.kt
+++ b/src/test/kotlin/concolic/ConcolicTests.kt
@@ -10,6 +10,7 @@ import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.ValueSource
 import java.io.File
 import kotlin.test.assertEquals
+import kotlin.test.assertNotNull
 
 @DisplayName("WARDuino concolic execution tests")
 class ConcolicTests : DebuggerTestBase() {
@@ -144,6 +145,8 @@ class ConcolicTests : DebuggerTestBase() {
         """.trimIndent())
             val result = getPathsFromWat(watString)
             assertEquals(2,result.getPathCount())
+            assertNotNull(result.paths.find { it.value == 5 })
+            assertNotNull(result.paths.find { it.value != 5 })
         }
 
         @Test
@@ -160,10 +163,12 @@ class ConcolicTests : DebuggerTestBase() {
         """.trimIndent())
             val result = getPathsFromWat(watString)
             assertEquals(2,result.getPathCount())
+            assertNotNull(result.paths.find { it.value == 5 })
+            assertNotNull(result.paths.find { it.value != 5 })
         }
 
         @Test
-        fun `Test wat floats less than`() {
+        fun `Test wat floats less than basic`() {
             val watString = makeWat($$"""
             i32.const 0
             call $chip_analog_read
@@ -176,10 +181,12 @@ class ConcolicTests : DebuggerTestBase() {
         """.trimIndent())
             val result = getPathsFromWat(watString)
             assertEquals(2,result.getPathCount())
+            assertNotNull(result.paths.find { it.value < 5 })
+            assertNotNull(result.paths.find { it.value >= 5 })
         }
 
         @Test
-        fun `Test wat floats less than 2`() {
+        fun `Test wat floats less than advanced`() {
             val watString = makeWat($$"""
             i32.const 0
             call $chip_analog_read
@@ -196,6 +203,32 @@ class ConcolicTests : DebuggerTestBase() {
         """.trimIndent())
             val result = getPathsFromWat(watString)
             assertEquals(2,result.getPathCount())
+            assertNotNull(result.paths.find { it.value < 16 })
+            assertNotNull(result.paths.find { it.value >= 16 })
+        }
+
+        @Test
+        fun `Test wat floats between`() {
+            val watString = makeWat($$"""
+            i32.const 0
+            call $chip_analog_read
+            local.tee 0
+            f32.convert_i32_s
+            f32.const 5.0
+            f32.lt
+            local.get 0
+            f32.convert_i32_s
+            f32.const 2.0
+            f32.gt
+            i32.and
+            if
+                nop
+            end
+        """.trimIndent())
+            val result = getPathsFromWat(watString)
+            assertEquals(2,result.getPathCount())
+            assertNotNull(result.paths.find { it.value < 5 && it.value > 2 })
+            assertNotNull(result.paths.find { it.value >= 5 || it.value <= 2})
         }
 
         @Test
@@ -213,6 +246,8 @@ class ConcolicTests : DebuggerTestBase() {
         """.trimIndent())
             val result = getPathsFromWat(watString)
             assertEquals(2,result.getPathCount())
+            assertNotNull(result.paths.find { it.value < 10 })
+            assertNotNull(result.paths.find { it.value >= 10 })
         }
 
         @Test

From 71e295b5b9a6bc845f8e5708d0300a060a4ea1eb Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Thu, 11 Sep 2025 11:57:13 +0200
Subject: [PATCH 04/13] Parameterize floats in between test

---
 src/test/kotlin/concolic/ConcolicTests.kt | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/test/kotlin/concolic/ConcolicTests.kt b/src/test/kotlin/concolic/ConcolicTests.kt
index c9084df..fbbbbf7 100644
--- a/src/test/kotlin/concolic/ConcolicTests.kt
+++ b/src/test/kotlin/concolic/ConcolicTests.kt
@@ -7,6 +7,7 @@ import org.junit.jupiter.api.DisplayName
 import org.junit.jupiter.api.Nested
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.CsvSource
 import org.junit.jupiter.params.provider.ValueSource
 import java.io.File
 import kotlin.test.assertEquals
@@ -207,18 +208,19 @@ class ConcolicTests : DebuggerTestBase() {
             assertNotNull(result.paths.find { it.value >= 16 })
         }
 
-        @Test
-        fun `Test wat floats between`() {
+        @ParameterizedTest(name = "Value in between {0} and {1}")
+        @CsvSource("2,5", "3,6", "-3,3", "-3,1", "500,502", "500.999,501.0001")
+        fun `Test wat floats between`(lower: Float, upper: Float) {
             val watString = makeWat($$"""
             i32.const 0
-            call $chip_analog_read
+            call $chip_analog_read (;Range 0 to 4096;)
             local.tee 0
             f32.convert_i32_s
-            f32.const 5.0
+            f32.const $$upper
             f32.lt
             local.get 0
             f32.convert_i32_s
-            f32.const 2.0
+            f32.const $$lower
             f32.gt
             i32.and
             if
@@ -227,8 +229,8 @@ class ConcolicTests : DebuggerTestBase() {
         """.trimIndent())
             val result = getPathsFromWat(watString)
             assertEquals(2,result.getPathCount())
-            assertNotNull(result.paths.find { it.value < 5 && it.value > 2 })
-            assertNotNull(result.paths.find { it.value >= 5 || it.value <= 2})
+            assertNotNull(result.paths.find { it.value < upper && it.value > lower })
+            assertNotNull(result.paths.find { it.value >= upper || it.value <= lower})
         }
 
         @Test

From fdf7a43ed889c428cb5e46a929a960a72e3729fe Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Thu, 11 Sep 2025 14:37:52 +0200
Subject: [PATCH 05/13] Add a few additional tests

---
 src/test/kotlin/concolic/ConcolicTests.kt | 43 +++++++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/src/test/kotlin/concolic/ConcolicTests.kt b/src/test/kotlin/concolic/ConcolicTests.kt
index fbbbbf7..bfa1683 100644
--- a/src/test/kotlin/concolic/ConcolicTests.kt
+++ b/src/test/kotlin/concolic/ConcolicTests.kt
@@ -252,6 +252,49 @@ class ConcolicTests : DebuggerTestBase() {
             assertNotNull(result.paths.find { it.value >= 10 })
         }
 
+        @Test
+        fun `Test wat floats i32_trunc_f32_s medium`() {
+            val watString = makeWat($$"""
+            i32.const 0
+            call $chip_analog_read
+            f32.convert_i32_s
+            f32.const 0x1.9p+5 (;=50;)
+            f32.sub
+            i32.trunc_f32_s
+            i32.const 25
+            i32.lt_s
+            if
+                nop
+            end
+        """.trimIndent())
+            val result = getPathsFromWat(watString)
+            assertEquals(2,result.getPathCount())
+            assertNotNull(result.paths.find { it.value < 75 })
+            assertNotNull(result.paths.find { it.value >= 75 })
+        }
+
+        @ParameterizedTest(name = "((value * {0}) as i32) < 50")
+        @ValueSource(floats = [0.488f, 2.3f, 3.14f, 10.42f, 0.1f, 0.02f, 0.0125f]) //, 0.01229f
+        fun `Test wat floats i32_trunc_f32_s medium 2`(v: Float) {
+            val watString = makeWat($$"""
+            i32.const 0
+            call $chip_analog_read
+            f32.convert_i32_s
+            f32.const $$v
+            f32.mul
+            i32.trunc_f32_s
+            i32.const 50
+            i32.lt_s
+            if
+                nop
+            end
+        """.trimIndent())
+            val result = getPathsFromWat(watString)
+            assertEquals(2,result.getPathCount())
+            assertNotNull(result.paths.find { it.value < 50 / v })
+            assertNotNull(result.paths.find { it.value >= 50 / v })
+        }
+
         @Test
         fun `Test wat floats i32_trunc_f32_s advanced`() {
             val watString = makeWat($$"""

From 5e128f11aca6feaa93a7678f29c24ca6ff01b951 Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Thu, 11 Sep 2025 17:56:43 +0200
Subject: [PATCH 06/13] Make test more strict

(Will fail on an older warduino version)
---
 src/test/kotlin/concolic/ConcolicTests.kt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/kotlin/concolic/ConcolicTests.kt b/src/test/kotlin/concolic/ConcolicTests.kt
index bfa1683..dac4013 100644
--- a/src/test/kotlin/concolic/ConcolicTests.kt
+++ b/src/test/kotlin/concolic/ConcolicTests.kt
@@ -274,7 +274,7 @@ class ConcolicTests : DebuggerTestBase() {
         }
 
         @ParameterizedTest(name = "((value * {0}) as i32) < 50")
-        @ValueSource(floats = [0.488f, 2.3f, 3.14f, 10.42f, 0.1f, 0.02f, 0.0125f]) //, 0.01229f
+        @ValueSource(floats = [0.488f, 2.3f, 3.14f, 10.42f, 0.1f, 0.02f, 0.0125f, 0.01222f, 0.0122129f])
         fun `Test wat floats i32_trunc_f32_s medium 2`(v: Float) {
             val watString = makeWat($$"""
             i32.const 0

From 69d6cb741226066864e43a93e88437336d80f70c Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Mon, 27 Oct 2025 14:43:10 +0100
Subject: [PATCH 07/13] Give a slightly more informative error message when
 finding more or less paths

---
 src/test/kotlin/concolic/ConcolicTests.kt | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/test/kotlin/concolic/ConcolicTests.kt b/src/test/kotlin/concolic/ConcolicTests.kt
index dac4013..a26f8f8 100644
--- a/src/test/kotlin/concolic/ConcolicTests.kt
+++ b/src/test/kotlin/concolic/ConcolicTests.kt
@@ -290,9 +290,9 @@ class ConcolicTests : DebuggerTestBase() {
             end
         """.trimIndent())
             val result = getPathsFromWat(watString)
-            assertEquals(2,result.getPathCount())
-            assertNotNull(result.paths.find { it.value < 50 / v })
-            assertNotNull(result.paths.find { it.value >= 50 / v })
+            assertEquals(2,result.getPathCount(), "Found more or less paths than expected!")
+            assertEquals(1, result.paths.count { it.value < 50 / v })
+            assertEquals(1, result.paths.count { it.value >= 50 / v })
         }
 
         @Test

From 76139a4d4b06ad634c7b024fc41d3a5280ff5e36 Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Wed, 29 Oct 2025 16:36:32 +0100
Subject: [PATCH 08/13] Add CI actions to run the mio setup process and execute
 the concolic tests

---
 .github/workflows/gradle.yml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index a71bdbc..f94efb2 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -49,6 +49,15 @@ jobs:
         name: MIO fatJar
         path: build/libs/mio.jar
 
+    - name: Install Z3
+      run: sudo apt install -y libz3-dev
+
+    - name: Setup MIO
+      run: ./gradlew setup
+
+    - name: Test concolic execution engine
+      run: ./gradlew test --tests concolic.ConcolicTests
+
   dependency-submission:
 
     runs-on: ubuntu-latest

From eab75ad5134b09772985e2259599b6f4832fef4d Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Wed, 29 Oct 2025 16:39:54 +0100
Subject: [PATCH 09/13] Make checkout in action recursive

---
 .github/workflows/gradle.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index f94efb2..fdc8ec3 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -18,6 +18,8 @@ jobs:
 
     steps:
     - uses: actions/checkout@v4
+      with:
+        submodules: recursive
     - name: Set up JDK 22
       uses: actions/setup-java@v4
       with:

From 9c4ab8f71c06f64790c7056fd8d1cb5f50469ac4 Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Wed, 29 Oct 2025 16:57:36 +0100
Subject: [PATCH 10/13] Add wabt to dependencies

---
 .github/workflows/gradle.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index fdc8ec3..754dd5e 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -51,14 +51,14 @@ jobs:
         name: MIO fatJar
         path: build/libs/mio.jar
 
-    - name: Install Z3
-      run: sudo apt install -y libz3-dev
+    - name: Install dependencies
+      run: sudo apt install -y libz3-dev wabt
 
     - name: Setup MIO
       run: ./gradlew setup
 
     - name: Test concolic execution engine
-      run: ./gradlew test --tests concolic.ConcolicTests
+      run: ./gradlew test --tests concolic.ConcolicTests --scan
 
   dependency-submission:
 

From 3b00b0ee16f5fc6d581125999cb7255e244e50ff Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Wed, 29 Oct 2025 17:21:21 +0100
Subject: [PATCH 11/13] Update gradle settings to include full stacktrace on
 failure

---
 .github/workflows/gradle.yml | 2 +-
 build.gradle.kts             | 5 +++++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index 754dd5e..4b44233 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -58,7 +58,7 @@ jobs:
       run: ./gradlew setup
 
     - name: Test concolic execution engine
-      run: ./gradlew test --tests concolic.ConcolicTests --scan
+      run: ./gradlew test --tests concolic.ConcolicTests
 
   dependency-submission:
 
diff --git a/build.gradle.kts b/build.gradle.kts
index 2db4e33..2aa2a2e 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -33,6 +33,11 @@ dependencies {
 
 tasks.test {
     useJUnitPlatform()
+
+    testLogging {
+        events("failed")
+        exceptionFormat = org.gradle.api.tasks.testing.logging.TestExceptionFormat.FULL
+    }
 }
 
 kotlin {

From 48b4124590bf29f04563af14512b9e881623fe64 Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Wed, 29 Oct 2025 17:26:02 +0100
Subject: [PATCH 12/13] Log standard streams for tests

---
 build.gradle.kts | 1 +
 1 file changed, 1 insertion(+)

diff --git a/build.gradle.kts b/build.gradle.kts
index 2aa2a2e..4d66eec 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -37,6 +37,7 @@ tasks.test {
     testLogging {
         events("failed")
         exceptionFormat = org.gradle.api.tasks.testing.logging.TestExceptionFormat.FULL
+        showStandardStreams = true
     }
 }
 

From 3ac9fb4979166bfe09b445ca73386648443cd897 Mon Sep 17 00:00:00 2001
From: MaartenS11 <maarten.steevens@gmail.com>
Date: Wed, 29 Oct 2025 18:01:11 +0100
Subject: [PATCH 13/13] Update symbolic warduino version

---
 WARDuino-symbolic | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/WARDuino-symbolic b/WARDuino-symbolic
index d0541f0..0458462 160000
--- a/WARDuino-symbolic
+++ b/WARDuino-symbolic
@@ -1 +1 @@
-Subproject commit d0541f02829208d5b524a1b9ca7fbe78d61f14eb
+Subproject commit 0458462e273dacb170fed7b514f90b228663d3f8