From 04a42c95943ae0a6c514b133a720bd94fc54b054 Mon Sep 17 00:00:00 2001
From: Daniel Schemmel <daniel@schemmel.net>
Date: Wed, 29 Jun 2022 23:47:22 +0100
Subject: Add a few simple solver tests

---
 test/Solver/ExerciseSolver.c.inc | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 test/Solver/ExerciseSolver.c.inc

(limited to 'test/Solver/ExerciseSolver.c.inc')

diff --git a/test/Solver/ExerciseSolver.c.inc b/test/Solver/ExerciseSolver.c.inc
new file mode 100644
index 00000000..0cd16a25
--- /dev/null
+++ b/test/Solver/ExerciseSolver.c.inc
@@ -0,0 +1,35 @@
+#include "klee/klee.h"
+
+#include <stddef.h>
+#include <stdio.h>
+
+// just play around with a few symbolic values to exercise the solver a bit
+int main(int argc, char **argv) {
+  unsigned arr[4];
+  klee_make_symbolic(arr, sizeof(arr), "arr");
+
+  arr[0] ^= arr[1];
+  arr[2] += arr[3];
+  arr[3] %= 8191;
+
+  {
+    size_t i;
+    klee_make_symbolic(&i, sizeof(i), "i");
+    if (i < sizeof(arr) / sizeof(*arr)) {
+      arr[i] = 0;
+    } else {
+      arr[0] = 0;
+    }
+  }
+
+  if (arr[0] + 8192 == arr[1]) {
+    arr[3] *= 2;
+  }
+
+  unsigned minimum = arr[0];
+  for (size_t i = 1; i < sizeof(arr) / sizeof(*arr); ++i) {
+    if (arr[i] < minimum) {
+      minimum = arr[i];
+    }
+  }
+}
-- 
cgit 1.4.1