Add an integration test for path satisfiability checking

intTests/test0061_path_sat/termination.c

@@ -0,0 +1,23 @@
+#include <stdint.h>
+
+uint64_t g1(uint64_t x) {
+  int i = 0;
+  uint64_t r = x;
+  do {
+    r = r+1;
+  } while ( i++ < 3 && r == 0 );
+  return r;
+}
+
+// NB the termination of the following loop
+// is a bit tricky because of the interaction
+// between short-cutting '&&' and the 'i++'
+// expression.
+uint64_t g2(uint64_t x) {
+  int i = 0;
+  uint64_t r = x;
+  do {
+    r = r+1;
+  } while ( r == 0 && i++ < 3 );
+  return r;
+}

intTests/test0061_path_sat/test.saw

@@ -0,0 +1,12 @@
+m <- llvm_load_module "termination.bc";
+
+let g_spec = do {
+  x <- crucible_fresh_var "x" (llvm_int 64);
+  crucible_execute_func [crucible_term x];
+  };
+
+crucible_llvm_verify m "g1" [] false g_spec z3;
+
+// NB: path sat checking is required for this
+// to terminate in a reasonable time
+crucible_llvm_verify m "g2" [] true g_spec z3;

intTests/test0061_path_sat/test.sh

@@ -0,0 +1 @@
+$SAW test.saw