diff --git a/Makefile b/Makefile
index e3d81539..b5c73a9b 100644
--- a/Makefile
+++ b/Makefile
@@ -92,7 +92,7 @@ $(eval $(call extradeps,dllist))
 MD = $(shell find docs -type f -name "*.md")
 CONSISTENT=$(patsubst %, _temp/consistent/%, $(MD))
 
-exercises: $(EXERCISES) $(SOLUTIONS) $(TESTED) $(VERIFIED) $(CONSISTENT)
+exercises: $(EXERCISES) $(SOLUTIONS) $(VERIFIED) $(CONSISTENT)
 
 CNWAR=--include $(MAKEFILE_DIR)/src/exercises/cn_wars.h
 CN=cn verify $(CNWAR)
diff --git a/runtime-test.sh b/runtime-test.sh
new file mode 100755
index 00000000..186afa0a
--- /dev/null
+++ b/runtime-test.sh
@@ -0,0 +1,234 @@
+#!/usr/bin/env bash
+set -euo pipefail -o noclobber
+
+function echo_and_err() {
+    printf "$1\n"
+    exit 1
+}
+
+[ $# -eq 0 ] || echo_and_err "USAGE: $0"
+
+RUNTIME_PREFIX="$OPAM_SWITCH_PREFIX/lib/cn/runtime"
+[ -d "${RUNTIME_PREFIX}" ] || echo_and_err "Could not find CN's runtime directory (looked at: '${RUNTIME_PREFIX}')"
+
+function exits_with_code() {
+  local file=$1
+  local expected_exit_code=$2
+
+  printf "[$file]... "
+  timeout 20 cn instrument --run "$file" --no-debug-info --tmp --print-steps -DCN_INSTRUMENT &> /dev/null
+  local result=$?
+
+  if [ $result -eq $expected_exit_code ]; then
+    printf "\033[32mPASS\033[0m\n"
+    return 0
+  else
+    printf "\033[31mFAIL\033[0m (Unexpected return code: $result)\n"
+    return 1
+  fi
+}
+
+function exits_with_error_code() {
+  local file=$1
+
+  printf "[$file]... "
+  timeout 20 cn instrument --run "$file" --no-debug-info --tmp --print-steps -DCN_INSTRUMENT &> /dev/null
+  local result=$?
+
+  if [ $result -gt 0 ]; then
+    printf "\033[32mPASS\033[0m\n"
+    return 0
+  else
+    printf "\033[31mFAIL\033[0m (Unexpected return code: $result)\n"
+    return 1
+  fi
+}
+
+SUCCESS=$(find src/example-archive/*/working -name '*.c' \
+            ! -name "00052.working.c" \
+            ! -name "00120.working.c" \
+            ! -name "00053.working.c" \
+            ! -name "00112.working.c" \
+            ! -name "00007.working.c" \
+            ! -name "00090.working.c" \
+            ! -name "00032.c" \
+            ! -name "00044.working.c" \
+            ! -name "00006.working.c" \
+            ! -name "00094.working.c" \
+            ! -name "00010_non_termination.c" \
+            ! -name "cast_1.c" \
+            ! -name "cast_2.c" \
+            ! -name "cast_3.c" \
+            ! -name "cast_4.c" \
+            ! -name "for_1.c" \
+            ! -name "for_3.c" \
+            ! -name "list_2.c" \
+            ! -name "list_3.c" \
+            ! -name "loop_2.c" \
+            ! -name "loop_6.c" \
+            ! -name "loop_8.c" \
+            ! -name "pointer_dec2.c" \
+            ! -name "string_1.c" \
+            ! -name "power_1.c" \
+            ! -name "power_2.c" \
+            ! -name "overflow_timeout_4var.c" \
+        )
+
+# Add files that fail for proof but are legitimate for testing and pass
+SUCCESS+=("\ 
+            src/example-archive/c-testsuite/broken/error-proof/00008.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00073.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00010.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00034.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00092.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00147.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00143.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00130.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00141.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00041.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00088.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00148.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00103.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00101.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00117.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00133.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00077.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00142.err1.c \
+            src/example-archive/c-testsuite/broken/error-proof/00040.err1.c \
+            src/example-archive/should-fail/broken/error-proof/overflow_neg_1.c \
+            src/example-archive/should-fail/broken/error-proof/overflow_neg_2.c \
+            src/example-archive/simple-examples/broken/error-proof/loop_4.c \
+            src/example-archive/simple-examples/broken/error-proof/case_timeout.c \
+            src/example-archive/simple-examples/broken/error-proof/ownership_1.c \
+")
+
+# Excluding files that:
+# - are ported from other test suites (time/bandwidth reasons)
+# - proof is not supposed to handle but testing passes for
+# - are buggy in Fulminate but should legitimately fail
+SHOULD_FAIL=$(find src/example-archive/*/broken -name '*.c' \
+            ! -path '*/Rust/*' \
+            ! -path '*/SAW/*' \
+            ! -path '*/dafny-tutorial/*' \
+            ! -path '*/java_program_verification_challenges/*' \
+            ! -path '*/coq-lemmas/*' \
+            ! -path '*/open-sut/*' \
+            ! -name "00008.err1.c" \
+            ! -name "00073.err1.c" \
+            ! -name "00010.err1.c" \
+            ! -name "00034.err1.c" \
+            ! -name "00092.err1.c" \
+            ! -name "00147.err1.c" \
+            ! -name "00143.err1.c" \
+            ! -name "00130.err1.c" \
+            ! -name "00141.err1.c" \
+            ! -name "00041.err1.c" \
+            ! -name "00088.err1.c" \
+            ! -name "00148.err1.c" \
+            ! -name "00103.err1.c" \
+            ! -name "00101.err1.c" \
+            ! -name "00117.err1.c" \
+            ! -name "00133.err1.c" \
+            ! -name "00077.err1.c" \
+            ! -name "00142.err1.c" \
+            ! -name "00040.err1.c" \
+            ! -name "overflow_neg_1.c" \
+            ! -name "overflow_neg_2.c" \
+            ! -name "loop_4.c" \
+            ! -name "case_timeout.c" \
+            ! -name "ownership_1.c" \
+            ! -name "00011_dependen_specifications.c" \
+            \
+            ! -name "00138.err1.c" \
+            ! -name "00026.err1.c" \
+            ! -name "00124.err1.c" \
+            ! -name "00151.err1.c" \
+            ! -name "00137.err1.c" \
+            ! -name "00058.err1.c" \
+            ! -name "00115.err1.c" \
+            ! -name "pointer_dec3.c" \
+            ! -name "self_ref_init.c" \
+        )
+
+# SHOULD_FAIL=""
+SHOULD_FAIL+=("src/example-archive/c-testsuite/working/00094.working.c ")
+# These examples use VIP, which is unsupported in Fulminate (Sep 2026)
+SHOULD_FAIL+=("\
+                src/example-archive/simple-examples/working/cast_1.c \
+                src/example-archive/simple-examples/working/cast_2.c \
+                src/example-archive/simple-examples/working/cast_3.c \
+                src/example-archive/simple-examples/working/cast_4.c")
+# For these list examples, I suspect the runtime lemma failure is legitimate 
+# and there is either something wrong with the specification, or the driver
+# constructs a list of the wrong shape.
+SHOULD_FAIL+=("\ 
+                src/example-archive/simple-examples/working/list_2.c \
+                src/example-archive/simple-examples/working/list_3.c \
+             ")
+
+# Loop timeout. loop_2 is infinite, loop_6 just a large # of iterations
+SHOULD_FAIL+=("\ 
+                src/example-archive/simple-examples/working/loop_2.c \
+                src/example-archive/simple-examples/working/loop_6.c \
+             ")
+
+# Uninterpreted functions unsupported for testing
+SHOULD_FAIL+=("\ 
+                src/example-archive/simple-examples/working/power_1.c \
+                src/example-archive/simple-examples/working/power_2.c \
+             ")
+
+BUGGY="\
+       src/example-archive/c-testsuite/working/00052.working.c \
+       src/example-archive/c-testsuite/working/00120.working.c \
+       src/example-archive/c-testsuite/working/00053.working.c \
+       src/example-archive/c-testsuite/working/00112.working.c \
+       src/example-archive/c-testsuite/working/00007.working.c \
+       src/example-archive/c-testsuite/working/00090.working.c \
+       src/example-archive/c-testsuite/working/00032.c \
+       src/example-archive/c-testsuite/working/00044.working.c \
+       src/example-archive/c-testsuite/working/00006.working.c \
+       src/example-archive/java_program_verification_challenges/working/00010_non_termination.c \
+       src/example-archive/simple-examples/working/for_1.c \
+       src/example-archive/simple-examples/working/for_3.c \
+       src/example-archive/simple-examples/working/loop_8.c \
+       src/example-archive/simple-examples/working/pointer_dec2.c \
+       src/example-archive/simple-examples/working/string_1.c \
+       src/example-archive/c-testsuite/broken/error-proof/00138.err1.c \
+       src/example-archive/c-testsuite/broken/error-proof/00026.err1.c \
+       src/example-archive/c-testsuite/broken/error-proof/00124.err1.c \
+       src/example-archive/c-testsuite/broken/error-proof/00151.err1.c \
+       src/example-archive/c-testsuite/broken/error-proof/00137.err1.c \
+       src/example-archive/c-testsuite/broken/error-proof/00058.err1.c \
+       src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c \
+       src/example-archive/simple-examples/broken/error-proof/self_ref_init.c \
+       src/example-archive/simple-examples/working/overflow_timeout_4var.c \
+    "
+
+
+FAILED=""
+
+for FILE in ${SUCCESS}; do
+  if ! exits_with_code "${FILE}" 0; then
+    FAILED+=" ${FILE}"
+  fi
+done
+
+for FILE in ${SHOULD_FAIL}; do
+  if ! exits_with_error_code "${FILE}"; then
+    FAILED+=" ${FILE}"
+  fi
+done
+
+for FILE in ${BUGGY}; do
+  if ! exits_with_error_code "${FILE}"; then
+    FAILED+=" ${FILE}"
+  fi
+done
+
+if [ -z "${FAILED}" ]; then
+  exit 0
+else
+  printf "\033[31mFAILED: ${FAILED}\033[0m\n"
+  exit 1
+fi
\ No newline at end of file
diff --git a/src/example-archive/SAW/working/00005.tutorial-double.c b/src/example-archive/SAW/working/00005.tutorial-double.c
index 8ea263cb..b55e0b7d 100644
--- a/src/example-archive/SAW/working/00005.tutorial-double.c
+++ b/src/example-archive/SAW/working/00005.tutorial-double.c
@@ -23,19 +23,27 @@ print "Done.";
 */
 
 int double_ref(int x)
-  /*@ requires let prod = 2i64 * (i64)x;
-               -2147483648i64 <= prod; prod<2147483647i64; 
-      ensures return == (i32) prod; 
+  /*@ requires let prod = 2 * x;
+               -2147483648 <= prod; prod < 2147483647; 
+      ensures return == prod; 
 @*/
 {
     return x * 2;
 }
 
 int double_imp(int x) 
-  /*@ requires let prod = 2i64 * (i64)x;
-               0i32 <= x; prod<2147483647i64; 
-      ensures return == (i32) prod; 
+  /*@ requires let prod = 2 * x;
+               0 <= x; prod < 2147483647; 
+      ensures return == prod; 
       @*/
 {
   return x << 1;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 42;
+  double_imp(x);
+  double_ref(x);
+}
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00008.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00008.err1.c
index e3a01bde..3e7dd5b0 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00008.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00008.err1.c
@@ -2,7 +2,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00010.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00010.err1.c
index d73fc2b4..5e717ba8 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00010.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00010.err1.c
@@ -2,7 +2,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	start:
 		goto next;
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00034.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00034.err1.c
index 397d5ef9..dafe0322 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00034.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00034.err1.c
@@ -2,7 +2,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00040.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00040.err1.c
index 356c9c2c..b9c28044 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00040.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00040.err1.c
@@ -47,7 +47,7 @@ go(int n, int x, int y)
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
         t = calloc(64, sizeof(int));
         go(0, 0, 0);
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00041.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00041.err1.c
index 24870251..e0e3e9aa 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00041.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00041.err1.c
@@ -3,7 +3,7 @@
 
 int
 main() 
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int n;
 	int t;
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00077.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00077.err1.c
index 963b79d4..47bcca36 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00077.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00077.err1.c
@@ -3,7 +3,10 @@
 int
 foo(int x[100])
 /*@ requires 
-			take PreX = each (u64 j; 0u64 <= j && j < 100u64) {RW<int>(x + j)}; @*/
+			take PreX = each (integer j; 0 <= j && j < 100) {RW<int>(x + j)}; 
+	ensures 
+			take PostX = each (integer j; 0 <= j && j < 100) {RW<int>(x + j)}; 
+@*/
 {
 	int y[100];
 	int *p;
@@ -45,11 +48,13 @@ foo(int x[100])
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x[100];
+	#ifndef CN_INSTRUMENT
 	assert(0); 
-	/*@ focus W<int>, 0u64; @*/
+	#endif
+	/*@ focus W<int>, 0; @*/
 	x[0] = 1000;
 	
 	return foo(x);
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00092.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00092.err1.c
index d5997966..fef2cbd0 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00092.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00092.err1.c
@@ -4,7 +4,7 @@ int a[] = {5, [2] = 2, 3};
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if (sizeof(a) != 4*sizeof(int))
 		return 1;
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00101.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00101.err1.c
index 7f5bb392..df612c59 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00101.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00101.err1.c
@@ -2,7 +2,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
   int c;
   c = 0;
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00103.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00103.err1.c
index 9251b5ec..8cde9439 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00103.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00103.err1.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	void *foo;
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00110.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00110.err1.c
index 7f6ab903..c51e1e84 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00110.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00110.err1.c
@@ -4,7 +4,7 @@ int x;
 int
 main()
 /*@ accesses x; @*/
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00115.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00115.err1.c
index cf821e54..e031725e 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00115.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00115.err1.c
@@ -4,8 +4,8 @@ char s[] = "a" B "c";
 
 int
 main()
-/*@ accesses s; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses s;
+	ensures return == 0; @*/
 {
 	if (s[0] != 'a')
 		return 1;
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00124.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00124.err1.c
index b7dadcc2..e8efd04a 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00124.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00124.err1.c
@@ -14,7 +14,7 @@ f1(int a, int b))(int c, int b)
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int (* (*p)(int a, int b))(int c, int d) = f1;
 
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00127.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00127.err1.c
index 029fd065..5a9f6ae8 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00127.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00127.err1.c
@@ -3,7 +3,7 @@ int c;
 int
 main()
 /*@ accesses c; @*/
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if(0) {
 		return 1;
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00130.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00130.err1.c
index ed2d0b67..df9a35e3 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00130.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00130.err1.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	char arr[2][4], (*p)[4], *q;
 	int v[4];
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00133.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00133.err1.c
index 65e1cdeb..b0a150a8 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00133.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00133.err1.c
@@ -1,5 +1,5 @@
 int main(void)
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int i;
 	unsigned u;
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00141.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00141.err1.c
index f0454b60..390825cf 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00141.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00141.err1.c
@@ -7,7 +7,7 @@
 
 int
 main(void)
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int foo, bar, foobar;
 
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00142.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00142.err1.c
index b378d1d3..466b8d6b 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00142.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00142.err1.c
@@ -10,8 +10,8 @@ int d;
 
 int
 main(void)
-/*@ accesses c; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses c;
+	ensures return == 0; @*/
 {
 	return c;
 }
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00147.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00147.err1.c
index 2155fc69..1c547f06 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00147.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00147.err1.c
@@ -2,7 +2,7 @@ int arr[3] = {[2] = 2, [0] = 0, [1] = 1};
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if(arr[0] != 0)
 		return 1;
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00148.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00148.err1.c
index df5b1709..229dac5b 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00148.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00148.err1.c
@@ -3,7 +3,7 @@ struct S arr[2] = {[1] = {3, 4}, [0] = {1, 2}};
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if(arr[0].a != 1)
 		return 1;
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00151.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00151.err1.c
index 6270645c..f709f39c 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00151.err1.c
+++ b/src/example-archive/c-testsuite/broken/error-proof/00151.err1.c
@@ -11,8 +11,8 @@ int arr[][3][5] = {
 
 int
 main(void)
-/*@ accesses arr; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses arr;
+	ensures return == 0; @*/
 {
 	return !(arr[0][1][4] == arr[1][1][4]);
 }
diff --git a/src/example-archive/c-testsuite/working/00001.working.c b/src/example-archive/c-testsuite/working/00001.working.c
index 73da83c6..070ac726 100644
--- a/src/example-archive/c-testsuite/working/00001.working.c
+++ b/src/example-archive/c-testsuite/working/00001.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00002.working.c b/src/example-archive/c-testsuite/working/00002.working.c
index 2fec5e0c..d437d697 100644
--- a/src/example-archive/c-testsuite/working/00002.working.c
+++ b/src/example-archive/c-testsuite/working/00002.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 3-3;
 }
diff --git a/src/example-archive/c-testsuite/working/00003.working.c b/src/example-archive/c-testsuite/working/00003.working.c
index ebed9764..06834888 100644
--- a/src/example-archive/c-testsuite/working/00003.working.c
+++ b/src/example-archive/c-testsuite/working/00003.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	
diff --git a/src/example-archive/c-testsuite/working/00004.working.c b/src/example-archive/c-testsuite/working/00004.working.c
index d69689ea..4d05559a 100644
--- a/src/example-archive/c-testsuite/working/00004.working.c
+++ b/src/example-archive/c-testsuite/working/00004.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	int *p;
diff --git a/src/example-archive/c-testsuite/working/00005.working.c b/src/example-archive/c-testsuite/working/00005.working.c
index 2eee2366..f591fb79 100644
--- a/src/example-archive/c-testsuite/working/00005.working.c
+++ b/src/example-archive/c-testsuite/working/00005.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	int *p;
diff --git a/src/example-archive/c-testsuite/working/00006.working.c b/src/example-archive/c-testsuite/working/00006.working.c
index c18e1c48..782ed6bd 100644
--- a/src/example-archive/c-testsuite/working/00006.working.c
+++ b/src/example-archive/c-testsuite/working/00006.working.c
@@ -1,12 +1,12 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 
 	x = 50;
 	while (x)
-		/*@ inv 0i32 <= x; x <= 50i32; @*/
+		/*@ inv 0 <= x; x <= 50; @*/
 		x = x - 1;
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00007.working.c b/src/example-archive/c-testsuite/working/00007.working.c
index dc79171c..64ab1ce2 100644
--- a/src/example-archive/c-testsuite/working/00007.working.c
+++ b/src/example-archive/c-testsuite/working/00007.working.c
@@ -1,18 +1,18 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	
 	x = 1;
 	for(x = 10; x; x = x - 1)
-		/*@ inv 0i32 <= x; x <= 10i32; @*/
+		/*@ inv 0 <= x; x <= 10; @*/
 		;
 	if(x)
 		return 1;
 	x = 10;
 	for (;x;)
-		/*@ inv 0i32 <= x; x <= 10i32; @*/
+		/*@ inv 0 <= x; x <= 10; @*/
 		x = x - 1;
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00011.working.c b/src/example-archive/c-testsuite/working/00011.working.c
index 034a3f27..483539d7 100644
--- a/src/example-archive/c-testsuite/working/00011.working.c
+++ b/src/example-archive/c-testsuite/working/00011.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	int y;
diff --git a/src/example-archive/c-testsuite/working/00012.working.c b/src/example-archive/c-testsuite/working/00012.working.c
index bfe9e7cf..9cd0bacd 100644
--- a/src/example-archive/c-testsuite/working/00012.working.c
+++ b/src/example-archive/c-testsuite/working/00012.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return (2 + 2) * 2 - 8;
 }
diff --git a/src/example-archive/c-testsuite/working/00013.working.c b/src/example-archive/c-testsuite/working/00013.working.c
index 72e60411..1fdfec34 100644
--- a/src/example-archive/c-testsuite/working/00013.working.c
+++ b/src/example-archive/c-testsuite/working/00013.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	int *p;
diff --git a/src/example-archive/c-testsuite/working/00014.working.c b/src/example-archive/c-testsuite/working/00014.working.c
index 1c52e491..70ecd8cc 100644
--- a/src/example-archive/c-testsuite/working/00014.working.c
+++ b/src/example-archive/c-testsuite/working/00014.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	int *p;
diff --git a/src/example-archive/c-testsuite/working/00015.working.c b/src/example-archive/c-testsuite/working/00015.working.c
index 20208686..3670f447 100644
--- a/src/example-archive/c-testsuite/working/00015.working.c
+++ b/src/example-archive/c-testsuite/working/00015.working.c
@@ -1,12 +1,12 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int arr[2];
 
-	/*@ focus W<int>, 0u64; @*/
+	/*@ focus W<int>, 0; @*/
 	arr[0] = 1;
-	/*@ focus W<int>, 1u64; @*/
+	/*@ focus W<int>, 1; @*/
 	arr[1] = 2;
 
 	return arr[0] + arr[1] - 3;
diff --git a/src/example-archive/c-testsuite/working/00016.working.c b/src/example-archive/c-testsuite/working/00016.working.c
index c02b8df3..c94c4df7 100644
--- a/src/example-archive/c-testsuite/working/00016.working.c
+++ b/src/example-archive/c-testsuite/working/00016.working.c
@@ -1,11 +1,11 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int arr[2];
 	int *p;
 	
-	/*@ focus W<int>, 1u64; @*/
+	/*@ focus W<int>, 1; @*/
 	p = &arr[1];
 	*p = 0;
 	return arr[1];
diff --git a/src/example-archive/c-testsuite/working/00017.working.c b/src/example-archive/c-testsuite/working/00017.working.c
index f02ca1d5..92e1e1a3 100644
--- a/src/example-archive/c-testsuite/working/00017.working.c
+++ b/src/example-archive/c-testsuite/working/00017.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	struct { int x; int y; } s;
 	
diff --git a/src/example-archive/c-testsuite/working/00018.working.c b/src/example-archive/c-testsuite/working/00018.working.c
index 50524bfe..3bcc429a 100644
--- a/src/example-archive/c-testsuite/working/00018.working.c
+++ b/src/example-archive/c-testsuite/working/00018.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 
 	struct S { int x; int y; } s;
diff --git a/src/example-archive/c-testsuite/working/00019.working.c b/src/example-archive/c-testsuite/working/00019.working.c
index 434f27f2..eb07846b 100644
--- a/src/example-archive/c-testsuite/working/00019.working.c
+++ b/src/example-archive/c-testsuite/working/00019.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	struct S { struct S *p; int x; } s;
 	
diff --git a/src/example-archive/c-testsuite/working/00020.working.c b/src/example-archive/c-testsuite/working/00020.working.c
index d445f848..c0a87fe1 100644
--- a/src/example-archive/c-testsuite/working/00020.working.c
+++ b/src/example-archive/c-testsuite/working/00020.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x, *p, **pp;
 	
diff --git a/src/example-archive/c-testsuite/working/00021.working.c b/src/example-archive/c-testsuite/working/00021.working.c
index e5fcf5ce..2ba058fb 100644
--- a/src/example-archive/c-testsuite/working/00021.working.c
+++ b/src/example-archive/c-testsuite/working/00021.working.c
@@ -1,18 +1,18 @@
 int
 foo(int a, int b)
 /*@ requires 
-			let mid = (2i64 + (i64) a);
-			let res = mid - (i64) b;  
-			(i64) MINi32() <= mid; mid <= (i64) MAXi32(); 
-			(i64) MINi32() <= res; res <= (i64) MAXi32(); 
-    ensures return == (2i32 + a) - b; @*/
+			let mid = (2 + a);
+			let res = mid - b;  
+			MINi32() <= mid; mid <= MAXi32(); 
+			MINi32() <= res; res <= MAXi32(); 
+    ensures return == (2 + a) - b; @*/
 {
 	return 2 + a - b;
 }
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return foo(1, 3);
 }
diff --git a/src/example-archive/c-testsuite/working/00022.working.c b/src/example-archive/c-testsuite/working/00022.working.c
index ff349533..6bf72a30 100644
--- a/src/example-archive/c-testsuite/working/00022.working.c
+++ b/src/example-archive/c-testsuite/working/00022.working.c
@@ -2,7 +2,7 @@ typedef int x;
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	x v;
 	v = 0;
diff --git a/src/example-archive/c-testsuite/working/00023.working.c b/src/example-archive/c-testsuite/working/00023.working.c
index ffd57ba5..af8364b3 100644
--- a/src/example-archive/c-testsuite/working/00023.working.c
+++ b/src/example-archive/c-testsuite/working/00023.working.c
@@ -3,7 +3,7 @@ int x;
 int
 main()
 /*@ accesses x;
-    ensures return == 0i32; @*/
+    ensures return == 0; @*/
 {
 	x = 0;
 	return x;
diff --git a/src/example-archive/c-testsuite/working/00024.working.c b/src/example-archive/c-testsuite/working/00024.working.c
index 8d3d6e72..e7aa4969 100644
--- a/src/example-archive/c-testsuite/working/00024.working.c
+++ b/src/example-archive/c-testsuite/working/00024.working.c
@@ -5,7 +5,7 @@ s v;
 int
 main()
 /*@ accesses v;
-    ensures return == 0i32; @*/
+    ensures return == 0; @*/
 {
 	v.x = 1;
 	v.y = 2;
diff --git a/src/example-archive/c-testsuite/working/00027.working.c b/src/example-archive/c-testsuite/working/00027.working.c
index c96bf759..95bf2fad 100644
--- a/src/example-archive/c-testsuite/working/00027.working.c
+++ b/src/example-archive/c-testsuite/working/00027.working.c
@@ -1,11 +1,13 @@
+/*@ lemma one_or_four() requires true; ensures 1 | 4 == 5; @*/
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	
 	x = 1;
 	x = x | 4;
+	/*@ apply one_or_four(); @*/
 	return x - 5;
 }
 
diff --git a/src/example-archive/c-testsuite/working/00028.working.c b/src/example-archive/c-testsuite/working/00028.working.c
index 362ccdae..5b04e815 100644
--- a/src/example-archive/c-testsuite/working/00028.working.c
+++ b/src/example-archive/c-testsuite/working/00028.working.c
@@ -1,11 +1,13 @@
+/*@ lemma one_and_three() requires true; ensures 1 & 3 == 1; @*/
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	
 	x = 1;
 	x = x & 3;
+	/*@ apply one_and_three(); @*/
 	return x - 1;
 }
 
diff --git a/src/example-archive/c-testsuite/working/00029.working.c b/src/example-archive/c-testsuite/working/00029.working.c
index 5d263763..d768f484 100644
--- a/src/example-archive/c-testsuite/working/00029.working.c
+++ b/src/example-archive/c-testsuite/working/00029.working.c
@@ -1,11 +1,13 @@
+/*@ lemma one_xor_three() requires true; ensures 1 ^ 3 == 2; @*/
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	
 	x = 1;
 	x = x ^ 3;
+	/*@ apply one_xor_three(); @*/
 	return x - 2;
 }
 
diff --git a/src/example-archive/c-testsuite/working/00030.working.c b/src/example-archive/c-testsuite/working/00030.working.c
index 1491225a..4f2b99fa 100644
--- a/src/example-archive/c-testsuite/working/00030.working.c
+++ b/src/example-archive/c-testsuite/working/00030.working.c
@@ -1,13 +1,13 @@
 int
 f()
-/*@ ensures return == 100i32; @*/
+/*@ ensures return == 100; @*/
 {
 	return 100;
 }
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if (f() > 1000)
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00031.working.c b/src/example-archive/c-testsuite/working/00031.working.c
index 29ed887a..a080fb73 100644
--- a/src/example-archive/c-testsuite/working/00031.working.c
+++ b/src/example-archive/c-testsuite/working/00031.working.c
@@ -1,20 +1,20 @@
 int
 zero()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
 
 int
 one()
-/*@ ensures return == 1i32; @*/
+/*@ ensures return == 1; @*/
 {
 	return 1;
 }
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	int y;
diff --git a/src/example-archive/c-testsuite/working/00032.c b/src/example-archive/c-testsuite/working/00032.c
index 6d2462ca..e7f571f8 100644
--- a/src/example-archive/c-testsuite/working/00032.c
+++ b/src/example-archive/c-testsuite/working/00032.c
@@ -2,14 +2,14 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int arr[2];
 	int *p;
 
-	/*@ focus W<int>, 0u64; @*/
+	/*@ focus W<int>, 0; @*/
 	arr[0] = 2;
-	/*@ focus W<int>, 1u64; @*/
+	/*@ focus W<int>, 1; @*/
 	arr[1] = 3;
 	p = &arr[0];
 	if(*(p++) != 2)
diff --git a/src/example-archive/c-testsuite/working/00033.working.c b/src/example-archive/c-testsuite/working/00033.working.c
index 058ac64b..4e1ca95e 100644
--- a/src/example-archive/c-testsuite/working/00033.working.c
+++ b/src/example-archive/c-testsuite/working/00033.working.c
@@ -6,8 +6,8 @@ effect()
         take Pre = RW<int>(&g);
     ensures 
         take Post = RW<int>(&g); 
-        Post == 1i32;  
-        return == 1i32; @*/
+        Post == 1;  
+        return == 1; @*/
 {
 	g = 1;
 	return 1;
@@ -19,7 +19,7 @@ main()
         take Pre = RW<int>(&g);
     ensures 
         take Post = RW<int>(&g);
-        return == 0i32; @*/
+        return == 0; @*/
 {
     int x;
     
diff --git a/src/example-archive/c-testsuite/working/00035.working.c b/src/example-archive/c-testsuite/working/00035.working.c
index a265120c..0770ade2 100644
--- a/src/example-archive/c-testsuite/working/00035.working.c
+++ b/src/example-archive/c-testsuite/working/00035.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	
diff --git a/src/example-archive/c-testsuite/working/00036.working.c b/src/example-archive/c-testsuite/working/00036.working.c
index 0f7924a8..0e6e6542 100644
--- a/src/example-archive/c-testsuite/working/00036.working.c
+++ b/src/example-archive/c-testsuite/working/00036.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	
diff --git a/src/example-archive/c-testsuite/working/00037.working.c b/src/example-archive/c-testsuite/working/00037.working.c
index 5840aa47..cb6d9847 100644
--- a/src/example-archive/c-testsuite/working/00037.working.c
+++ b/src/example-archive/c-testsuite/working/00037.working.c
@@ -1,10 +1,10 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x[2];
 	int *p;
-	/*@ focus W<int>, 1u64; @*/
+	/*@ focus W<int>, 1; @*/
 	x[1] = 7;
 	p = &x[0];
 	p = p + 1;
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00038.err1.c b/src/example-archive/c-testsuite/working/00038.c
similarity index 90%
rename from src/example-archive/c-testsuite/broken/error-proof/00038.err1.c
rename to src/example-archive/c-testsuite/working/00038.c
index def767d3..5e2229bc 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00038.err1.c
+++ b/src/example-archive/c-testsuite/working/00038.c
@@ -3,7 +3,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x, *p;
 
diff --git a/src/example-archive/c-testsuite/working/00039.working.c b/src/example-archive/c-testsuite/working/00039.working.c
index 0fa3defc..218be556 100644
--- a/src/example-archive/c-testsuite/working/00039.working.c
+++ b/src/example-archive/c-testsuite/working/00039.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	void *p;
 	int x;
diff --git a/src/example-archive/c-testsuite/working/00043.working.c b/src/example-archive/c-testsuite/working/00043.working.c
index be5e0b47..6689409e 100644
--- a/src/example-archive/c-testsuite/working/00043.working.c
+++ b/src/example-archive/c-testsuite/working/00043.working.c
@@ -8,7 +8,7 @@ struct s {
 
 int
 main() 
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
     struct s v;
     v.x = 1;
diff --git a/src/example-archive/c-testsuite/working/00044.working.c b/src/example-archive/c-testsuite/working/00044.working.c
index 0962a67f..cda6dedf 100644
--- a/src/example-archive/c-testsuite/working/00044.working.c
+++ b/src/example-archive/c-testsuite/working/00044.working.c
@@ -6,7 +6,7 @@ struct T {
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	struct T v;
 	{ struct T { int z; }; }
diff --git a/src/example-archive/c-testsuite/working/00045.working.c b/src/example-archive/c-testsuite/working/00045.working.c
index 85ff6525..36fead56 100644
--- a/src/example-archive/c-testsuite/working/00045.working.c
+++ b/src/example-archive/c-testsuite/working/00045.working.c
@@ -6,10 +6,10 @@ int
 main()
 /*@ accesses x, y, p;
     requires
-			x == 5i32;
-			y == 6i64;
+			x == 5;
+			y == 6;
 			p == &x;
-    ensures return == 0i32; @*/
+    ensures return == 0; @*/
 {
 	if (x != 5)
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00047.working.c b/src/example-archive/c-testsuite/working/00047.working.c
index 226fa68d..84fdd61e 100644
--- a/src/example-archive/c-testsuite/working/00047.working.c
+++ b/src/example-archive/c-testsuite/working/00047.working.c
@@ -4,10 +4,10 @@ int
 main()
 /*@ accesses s;
     requires 
-			s.a == 1i32;
-			s.b == 2i32; 
-			s.c == 3i32;
-    ensures return == 0i32; @*/
+			s.a == 1;
+			s.b == 2; 
+			s.c == 3;
+    ensures return == 0; @*/
 {
 	if (s.a != 1)
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00048.working.c b/src/example-archive/c-testsuite/working/00048.working.c
index 9904be52..1f8e925b 100644
--- a/src/example-archive/c-testsuite/working/00048.working.c
+++ b/src/example-archive/c-testsuite/working/00048.working.c
@@ -5,9 +5,9 @@ int
 main()
 /*@ accesses s;
     requires 
-			s.a == 1i32;
-			s.b == 2i32;
-    ensures return == 0i32; @*/
+			s.a == 1;
+			s.b == 2;
+    ensures return == 0; @*/
 {
 	if(s.a != 1)
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00049.working.c b/src/example-archive/c-testsuite/working/00049.working.c
index 57501452..88178c29 100644
--- a/src/example-archive/c-testsuite/working/00049.working.c
+++ b/src/example-archive/c-testsuite/working/00049.working.c
@@ -7,9 +7,9 @@ int
 main()
 /*@ accesses s, x;
     requires
-			x == 10i32;
-			s.p == &x; s.a == 1i32;
-    ensures return == 0i32; @*/
+			x == 10;
+			s.p == &x; s.a == 1;
+    ensures return == 0; @*/
 {
 	if(s.a != 1)
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00052.working.c b/src/example-archive/c-testsuite/working/00052.working.c
index 8aeb1ec7..d3f728f3 100644
--- a/src/example-archive/c-testsuite/working/00052.working.c
+++ b/src/example-archive/c-testsuite/working/00052.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	struct T { int x; };
 	{
diff --git a/src/example-archive/c-testsuite/working/00053.working.c b/src/example-archive/c-testsuite/working/00053.working.c
index df1402f2..fb121432 100644
--- a/src/example-archive/c-testsuite/working/00053.working.c
+++ b/src/example-archive/c-testsuite/working/00053.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	struct T { int x; } s1;
 	s1.x = 1;
diff --git a/src/example-archive/c-testsuite/working/00054.working.c b/src/example-archive/c-testsuite/working/00054.working.c
index 1a2feed1..da38216d 100644
--- a/src/example-archive/c-testsuite/working/00054.working.c
+++ b/src/example-archive/c-testsuite/working/00054.working.c
@@ -6,7 +6,7 @@ enum E {
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	enum E e;
 
diff --git a/src/example-archive/c-testsuite/working/00055.working.c b/src/example-archive/c-testsuite/working/00055.working.c
index b5ce16c9..48fa422a 100644
--- a/src/example-archive/c-testsuite/working/00055.working.c
+++ b/src/example-archive/c-testsuite/working/00055.working.c
@@ -6,7 +6,7 @@ enum E {
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	enum E e;
 
diff --git a/src/example-archive/c-testsuite/working/00057.working.c b/src/example-archive/c-testsuite/working/00057.working.c
index 1bddb63b..9b38fb3d 100644
--- a/src/example-archive/c-testsuite/working/00057.working.c
+++ b/src/example-archive/c-testsuite/working/00057.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	char a[16], b[16];
 	
diff --git a/src/example-archive/c-testsuite/working/00059.working.c b/src/example-archive/c-testsuite/working/00059.working.c
index ea8d4fac..dec78e6f 100644
--- a/src/example-archive/c-testsuite/working/00059.working.c
+++ b/src/example-archive/c-testsuite/working/00059.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if ('a' != 97)
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00060.working.c b/src/example-archive/c-testsuite/working/00060.working.c
index 0624fac9..86ec9cde 100644
--- a/src/example-archive/c-testsuite/working/00060.working.c
+++ b/src/example-archive/c-testsuite/working/00060.working.c
@@ -2,7 +2,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	/*
 		multiline
diff --git a/src/example-archive/c-testsuite/working/00061.working.c b/src/example-archive/c-testsuite/working/00061.working.c
index 7c704c82..808afe89 100644
--- a/src/example-archive/c-testsuite/working/00061.working.c
+++ b/src/example-archive/c-testsuite/working/00061.working.c
@@ -1,7 +1,7 @@
 #define FOO 0
 
 int main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return FOO;
 }
diff --git a/src/example-archive/c-testsuite/working/00062.working.c b/src/example-archive/c-testsuite/working/00062.working.c
index 29570d9d..862837de 100644
--- a/src/example-archive/c-testsuite/working/00062.working.c
+++ b/src/example-archive/c-testsuite/working/00062.working.c
@@ -17,8 +17,8 @@ int x = 0;
 int
 main()
 /*@ accesses x;
-    requires x == 0i32;
-    ensures return == 0i32; @*/
+    requires x == 0;
+    ensures return == 0; @*/
 {
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00063.working.c b/src/example-archive/c-testsuite/working/00063.working.c
index d7a552fd..3459d9d5 100644
--- a/src/example-archive/c-testsuite/working/00063.working.c
+++ b/src/example-archive/c-testsuite/working/00063.working.c
@@ -15,7 +15,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return BAR;
 }
diff --git a/src/example-archive/c-testsuite/working/00065.working.c b/src/example-archive/c-testsuite/working/00065.working.c
index 119b9d11..31240ed5 100644
--- a/src/example-archive/c-testsuite/working/00065.working.c
+++ b/src/example-archive/c-testsuite/working/00065.working.c
@@ -3,7 +3,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return ADD(1, 2) - 3;
 }
diff --git a/src/example-archive/c-testsuite/working/00066.working.c b/src/example-archive/c-testsuite/working/00066.working.c
index eb818173..9346d6eb 100644
--- a/src/example-archive/c-testsuite/working/00066.working.c
+++ b/src/example-archive/c-testsuite/working/00066.working.c
@@ -4,7 +4,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if(FOO(1, 2, A) != 6)
 		return 1 SEMI
diff --git a/src/example-archive/c-testsuite/working/00067.working.c b/src/example-archive/c-testsuite/working/00067.working.c
index ba1ac25b..1e042962 100644
--- a/src/example-archive/c-testsuite/working/00067.working.c
+++ b/src/example-archive/c-testsuite/working/00067.working.c
@@ -14,8 +14,8 @@ int x = 1;
 
 int main()
 /*@ accesses x;
-    requires x == 0i32;
-    ensures return == 0i32; @*/
+    requires x == 0;
+    ensures return == 0; @*/
 {
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00068.working.c b/src/example-archive/c-testsuite/working/00068.working.c
index a3e758b1..fc72fbe6 100644
--- a/src/example-archive/c-testsuite/working/00068.working.c
+++ b/src/example-archive/c-testsuite/working/00068.working.c
@@ -9,8 +9,8 @@ X
 int
 main()
 /*@ accesses x;
-    requires x == 0i32;
-    ensures return == 0i32; @*/
+    requires x == 0;
+    ensures return == 0; @*/
 {
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00069.working.c b/src/example-archive/c-testsuite/working/00069.working.c
index 66e7b70a..dd3cc20a 100644
--- a/src/example-archive/c-testsuite/working/00069.working.c
+++ b/src/example-archive/c-testsuite/working/00069.working.c
@@ -9,8 +9,8 @@ int x = 0;
 int
 main()
 /*@ accesses x;
-    requires x == 0i32;
-    ensures return == 0i32; @*/
+    requires x == 0;
+    ensures return == 0; @*/
 {
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00070.working.c b/src/example-archive/c-testsuite/working/00070.working.c
index 382bc2c9..6883490a 100644
--- a/src/example-archive/c-testsuite/working/00070.working.c
+++ b/src/example-archive/c-testsuite/working/00070.working.c
@@ -11,8 +11,8 @@ X
 int
 main()
 /*@ accesses x;
-    requires x == 0i32;
-    ensures return == 0i32; @*/
+    requires x == 0;
+    ensures return == 0; @*/
 {
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00071.working.c b/src/example-archive/c-testsuite/working/00071.working.c
index c7085fe7..15284e22 100644
--- a/src/example-archive/c-testsuite/working/00071.working.c
+++ b/src/example-archive/c-testsuite/working/00071.working.c
@@ -7,7 +7,7 @@ FAIL
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00072.working.c b/src/example-archive/c-testsuite/working/00072.working.c
index 34ee6500..4afa5e9b 100644
--- a/src/example-archive/c-testsuite/working/00072.working.c
+++ b/src/example-archive/c-testsuite/working/00072.working.c
@@ -1,10 +1,10 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int arr[2];
 	int *p;
-	/*@ focus W<int>, 1u64; @*/
+	/*@ focus W<int>, 1; @*/
 	p = &arr[0];
 	p += 1;
 	*p = 123;
diff --git a/src/example-archive/c-testsuite/working/00074.working.c b/src/example-archive/c-testsuite/working/00074.working.c
index b063e276..0598b9d6 100644
--- a/src/example-archive/c-testsuite/working/00074.working.c
+++ b/src/example-archive/c-testsuite/working/00074.working.c
@@ -26,7 +26,7 @@ int x = 0;
 #if X
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00075.working.c b/src/example-archive/c-testsuite/working/00075.working.c
index d9126328..fdc1b1d9 100644
--- a/src/example-archive/c-testsuite/working/00075.working.c
+++ b/src/example-archive/c-testsuite/working/00075.working.c
@@ -160,7 +160,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00076.working.c b/src/example-archive/c-testsuite/working/00076.working.c
index 9dd5285c..adbcab83 100644
--- a/src/example-archive/c-testsuite/working/00076.working.c
+++ b/src/example-archive/c-testsuite/working/00076.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if(0 ? 1 : 0)
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00078.working.c b/src/example-archive/c-testsuite/working/00078.working.c
index b94187b0..780e23f1 100644
--- a/src/example-archive/c-testsuite/working/00078.working.c
+++ b/src/example-archive/c-testsuite/working/00078.working.c
@@ -4,14 +4,14 @@ f1(char *p)
 			take PreP = RW<char>(p);
     ensures 
 			take PostP = RW<char>(p);
-			return == 1i32 + (i32) PreP; @*/
+			return == 1 + PreP; @*/
 {
 	return *p+1;
 }
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	char s = 1;
 	int v[1000];
diff --git a/src/example-archive/c-testsuite/working/00079.working.c b/src/example-archive/c-testsuite/working/00079.working.c
index a249bc6c..0979d3a4 100644
--- a/src/example-archive/c-testsuite/working/00079.working.c
+++ b/src/example-archive/c-testsuite/working/00079.working.c
@@ -2,7 +2,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	int y;
diff --git a/src/example-archive/c-testsuite/working/00081.working.c b/src/example-archive/c-testsuite/working/00081.working.c
index 7ac2a241..0d35e6fe 100644
--- a/src/example-archive/c-testsuite/working/00081.working.c
+++ b/src/example-archive/c-testsuite/working/00081.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	long long x;
 	
diff --git a/src/example-archive/c-testsuite/working/00082.working.c b/src/example-archive/c-testsuite/working/00082.working.c
index 9cd1854c..6e5dce9e 100644
--- a/src/example-archive/c-testsuite/working/00082.working.c
+++ b/src/example-archive/c-testsuite/working/00082.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	unsigned long long x;
 	
diff --git a/src/example-archive/c-testsuite/working/00083.working.c b/src/example-archive/c-testsuite/working/00083.working.c
index 5eb423d7..a27ea38e 100644
--- a/src/example-archive/c-testsuite/working/00083.working.c
+++ b/src/example-archive/c-testsuite/working/00083.working.c
@@ -3,7 +3,7 @@
 int
 one(int a)
 /*@ ensures 
-			return == (a != 1i32 ? 1i32 : 0i32); @*/
+			return == (a != 1 ? 1 : 0); @*/
 {
 	if (a != 1)
 		return 1;
@@ -14,8 +14,8 @@ one(int a)
 int
 two(int a, int b)
 /*@ ensures 
-			return == (a != 1i32 ? 1i32 : 
-									(b != 2i32 ? 1i32 : 0i32 )); @*/
+			return == (a != 1 ? 1 : 
+									(b != 2 ? 1 : 0 )); @*/
 {
 	if (a != 1)
 		return 1;
@@ -28,9 +28,9 @@ two(int a, int b)
 int
 three(int a, int b, int c)
 /*@ ensures 
-			return == (a != 1i32 ? 1i32 : 
-									(b != 2i32 ? 1i32 : 
-										(c != 3i32 ? 1i32 : 0i32 ))); @*/
+			return == (a != 1 ? 1 : 
+									(b != 2 ? 1 : 
+										(c != 3 ? 1 : 0 ))); @*/
 {
 	if (a != 1)
 		return 1;
@@ -44,7 +44,7 @@ three(int a, int b, int c)
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if (CALL(one, 1))
 		return 2;
diff --git a/src/example-archive/c-testsuite/working/00084.working.c b/src/example-archive/c-testsuite/working/00084.working.c
index 0501a4ff..510ec841 100644
--- a/src/example-archive/c-testsuite/working/00084.working.c
+++ b/src/example-archive/c-testsuite/working/00084.working.c
@@ -2,7 +2,7 @@
 
 int
 none()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
@@ -10,7 +10,7 @@ none()
 int
 one(int a)
 /*@ ensures 
-			return == (a != 1i32 ? 1i32 : 0i32); @*/
+			return == (a != 1 ? 1 : 0); @*/
 {
 	if (a != 1)
 		return 1;
@@ -21,8 +21,8 @@ one(int a)
 int
 two(int a, int b)
 /*@ ensures 
-			return == (a != 1i32 ? 1i32 : 
-									(b != 2i32 ? 1i32 : 0i32 )); @*/
+			return == (a != 1 ? 1 : 
+									(b != 2 ? 1 : 0 )); @*/
 {
 	if (a != 1)
 		return 1;
@@ -35,9 +35,9 @@ two(int a, int b)
 int
 three(int a, int b, int c)
 /*@ ensures 
-			return == (a != 1i32 ? 1i32 : 
-									(b != 2i32 ? 1i32 : 
-										(c != 3i32 ? 1i32 : 0i32 ))); @*/
+			return == (a != 1 ? 1 : 
+									(b != 2 ? 1 : 
+										(c != 3 ? 1 : 0 ))); @*/
 {
 	if (a != 1)
 		return 1;
@@ -51,7 +51,7 @@ three(int a, int b, int c)
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if (none(ARGS()))
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00085.working.c b/src/example-archive/c-testsuite/working/00085.working.c
index cdffc85e..54e4150a 100644
--- a/src/example-archive/c-testsuite/working/00085.working.c
+++ b/src/example-archive/c-testsuite/working/00085.working.c
@@ -6,7 +6,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if (ZERO_0())
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00086.working.c b/src/example-archive/c-testsuite/working/00086.working.c
index 4fa1b93a..1e7a8c17 100644
--- a/src/example-archive/c-testsuite/working/00086.working.c
+++ b/src/example-archive/c-testsuite/working/00086.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	short x;
 	
diff --git a/src/example-archive/c-testsuite/working/00090.working.c b/src/example-archive/c-testsuite/working/00090.working.c
index 245882bc..9bc284e5 100644
--- a/src/example-archive/c-testsuite/working/00090.working.c
+++ b/src/example-archive/c-testsuite/working/00090.working.c
@@ -6,15 +6,15 @@ int
 main()
 /*@ accesses a;
     requires 
-			a[0u64] == 0i32; 
-			a[1u64] == 1i32; 
-			a[2u64] == 2i32; 
+			a[0] == 0; 
+			a[1] == 1; 
+			a[2] == 2; 
 
-    ensures return == 0i32; @*/
+    ensures return == 0; @*/
 {
-	/*@ focus RW<int>, 0u64; @*/
-	/*@ focus RW<int>, 1u64; @*/
-	/*@ focus RW<int>, 2u64; @*/
+	/*@ focus RW<int>, 0; @*/
+	/*@ focus RW<int>, 1; @*/
+	/*@ focus RW<int>, 2; @*/
 	if (a[0] != 0)
 		return 1;
 	if (a[1] != 1)
diff --git a/src/example-archive/c-testsuite/broken/error-proof/00093.err1.c b/src/example-archive/c-testsuite/working/00093.c
similarity index 82%
rename from src/example-archive/c-testsuite/broken/error-proof/00093.err1.c
rename to src/example-archive/c-testsuite/working/00093.c
index 674eec8c..8e40689e 100644
--- a/src/example-archive/c-testsuite/broken/error-proof/00093.err1.c
+++ b/src/example-archive/c-testsuite/working/00093.c
@@ -4,7 +4,7 @@ int a[] = {1, 2, 3, 4};
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	if (sizeof(a) != 4*sizeof(int))
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00094.working.c b/src/example-archive/c-testsuite/working/00094.working.c
index 0ea13925..b59a8610 100644
--- a/src/example-archive/c-testsuite/working/00094.working.c
+++ b/src/example-archive/c-testsuite/working/00094.working.c
@@ -1,7 +1,7 @@
-extern int x;
+extern int x; // Testing fails -- linker error because x not defined anywhere
 
 int main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00096.working.c b/src/example-archive/c-testsuite/working/00096.working.c
index 0bb5e671..e6c7ccff 100644
--- a/src/example-archive/c-testsuite/working/00096.working.c
+++ b/src/example-archive/c-testsuite/working/00096.working.c
@@ -3,7 +3,7 @@ int x, x = 3, x;
 int
 main()
 /*@ accesses x;
-    ensures return == 0i32; @*/
+    ensures return == 0; @*/
 {
 	if (x != 3)
 		return 0;
diff --git a/src/example-archive/c-testsuite/working/00097.working.c b/src/example-archive/c-testsuite/working/00097.working.c
index e0bad69f..dee0d259 100644
--- a/src/example-archive/c-testsuite/working/00097.working.c
+++ b/src/example-archive/c-testsuite/working/00097.working.c
@@ -9,7 +9,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00098.working.c b/src/example-archive/c-testsuite/working/00098.working.c
index 9ca5ea45..099a0464 100644
--- a/src/example-archive/c-testsuite/working/00098.working.c
+++ b/src/example-archive/c-testsuite/working/00098.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return L'\0';
 }
diff --git a/src/example-archive/c-testsuite/working/00099.working.c b/src/example-archive/c-testsuite/working/00099.working.c
index b2e89c55..48d80782 100644
--- a/src/example-archive/c-testsuite/working/00099.working.c
+++ b/src/example-archive/c-testsuite/working/00099.working.c
@@ -8,7 +8,7 @@ vecresize(Vec *v, int cap)
 }
 
 int main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00100.working.c b/src/example-archive/c-testsuite/working/00100.working.c
index e4e9e850..fd18cd03 100644
--- a/src/example-archive/c-testsuite/working/00100.working.c
+++ b/src/example-archive/c-testsuite/working/00100.working.c
@@ -1,13 +1,13 @@
 int
 foo(void)
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return foo();
 }
diff --git a/src/example-archive/c-testsuite/working/00102.working.c b/src/example-archive/c-testsuite/working/00102.working.c
index 40b9b4cc..df1a30f5 100644
--- a/src/example-archive/c-testsuite/working/00102.working.c
+++ b/src/example-archive/c-testsuite/working/00102.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x;
 	
diff --git a/src/example-archive/c-testsuite/working/00105.working.c b/src/example-archive/c-testsuite/working/00105.working.c
index 87e719d1..d259d491 100644
--- a/src/example-archive/c-testsuite/working/00105.working.c
+++ b/src/example-archive/c-testsuite/working/00105.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int i;
 
diff --git a/src/example-archive/c-testsuite/working/00106.working.c b/src/example-archive/c-testsuite/working/00106.working.c
index 8f8e60db..58b3df85 100644
--- a/src/example-archive/c-testsuite/working/00106.working.c
+++ b/src/example-archive/c-testsuite/working/00106.working.c
@@ -3,7 +3,7 @@ struct S2 { struct S1 s1; };
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	struct S2 s2;
 	s2.s1.x = 1;
diff --git a/src/example-archive/c-testsuite/working/00107.working.c b/src/example-archive/c-testsuite/working/00107.working.c
index 643cf510..bf72ab17 100644
--- a/src/example-archive/c-testsuite/working/00107.working.c
+++ b/src/example-archive/c-testsuite/working/00107.working.c
@@ -4,8 +4,8 @@ myint x = (myint)1;
 int
 main(void)
 /*@ accesses x;
-    requires x == 1i32;
-    ensures return == 0i32; @*/
+    requires x == 1;
+    ensures return == 0; @*/
 {
 	return x-1;
 }
diff --git a/src/example-archive/c-testsuite/working/00108.working.c b/src/example-archive/c-testsuite/working/00108.working.c
index fa38722d..2d227893 100644
--- a/src/example-archive/c-testsuite/working/00108.working.c
+++ b/src/example-archive/c-testsuite/working/00108.working.c
@@ -4,7 +4,7 @@ int foo(void);
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return FOO;
 }
diff --git a/src/example-archive/c-testsuite/working/00109.working.c b/src/example-archive/c-testsuite/working/00109.working.c
index 3713bf52..2337ea8e 100644
--- a/src/example-archive/c-testsuite/working/00109.working.c
+++ b/src/example-archive/c-testsuite/working/00109.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	int x = 0;
 	int y = 1;
diff --git a/src/example-archive/c-testsuite/working/00111.working.c b/src/example-archive/c-testsuite/working/00111.working.c
index db020bbb..a0497721 100644
--- a/src/example-archive/c-testsuite/working/00111.working.c
+++ b/src/example-archive/c-testsuite/working/00111.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	short s = 1;
 	long l = 1;
diff --git a/src/example-archive/c-testsuite/working/00114.working.c b/src/example-archive/c-testsuite/working/00114.working.c
index 77347f53..72df2887 100644
--- a/src/example-archive/c-testsuite/working/00114.working.c
+++ b/src/example-archive/c-testsuite/working/00114.working.c
@@ -2,7 +2,7 @@ int main(void);
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00116.working.c b/src/example-archive/c-testsuite/working/00116.working.c
index 9ecd47e8..34622066 100644
--- a/src/example-archive/c-testsuite/working/00116.working.c
+++ b/src/example-archive/c-testsuite/working/00116.working.c
@@ -7,7 +7,7 @@ f(int f)
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return f(0);
 }
diff --git a/src/example-archive/c-testsuite/working/00118.working.c b/src/example-archive/c-testsuite/working/00118.working.c
index aedea0bf..ae3714ea 100644
--- a/src/example-archive/c-testsuite/working/00118.working.c
+++ b/src/example-archive/c-testsuite/working/00118.working.c
@@ -1,6 +1,6 @@
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	struct { int x; } s = { 0 };
 	return s.x;
diff --git a/src/example-archive/c-testsuite/working/00120.working.c b/src/example-archive/c-testsuite/working/00120.working.c
index 66aaa232..acc968a9 100644
--- a/src/example-archive/c-testsuite/working/00120.working.c
+++ b/src/example-archive/c-testsuite/working/00120.working.c
@@ -5,7 +5,7 @@ struct {
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return X;
 }
diff --git a/src/example-archive/c-testsuite/working/00121.working.c b/src/example-archive/c-testsuite/working/00121.working.c
index 8a5b75ca..1b795a74 100644
--- a/src/example-archive/c-testsuite/working/00121.working.c
+++ b/src/example-archive/c-testsuite/working/00121.working.c
@@ -3,7 +3,7 @@ int f(int a), g(int a), a;
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return f(1) - g(1);
 }
diff --git a/src/example-archive/c-testsuite/working/00122.working.c b/src/example-archive/c-testsuite/working/00122.working.c
index c930abca..fcaaf496 100644
--- a/src/example-archive/c-testsuite/working/00122.working.c
+++ b/src/example-archive/c-testsuite/working/00122.working.c
@@ -1,7 +1,7 @@
 #define F(a, b) a
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return F(, 1) 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00128.working.c b/src/example-archive/c-testsuite/working/00128.working.c
index e52950f0..919bd761 100644
--- a/src/example-archive/c-testsuite/working/00128.working.c
+++ b/src/example-archive/c-testsuite/working/00128.working.c
@@ -16,23 +16,23 @@ int
 main(void)
 /*@ accesses a, b, c, d, e, f, g, h, i, j, k;
 
-    requires (i128) MINi32() <= (i128) b; (i128) b <= (i128) MAXi32();
-
-             (i128) MINu8() <= (i128) d; (i128) d <= (i128) MAXu8();
-             (i128) MINu8() <= (i128) f; (i128) f <= (i128) MAXu8();
-             (i128) MINu8() <= (i128) h; (i128) h <= (i128) MAXu8();
-             (i128) MINu8() <= (i128) i; (i128) i <= (i128) MAXu8();
-             (i128) MINu8() <= (i128) j; (i128) j <= (i128) MAXu8();
-
-             (i128) MINi8() <= (i128) e; (i128) e <= (i128) MAXi8();
-             (i128) MINi8() <= (i128) f; (i128) f <= (i128) MAXi8();
-             (i128) MINi8() <= (i128) g; (i128) g <= (i128) MAXi8();
-             (i128) MINi8() <= (i128) h; (i128) h <= (i128) MAXi8();
-             (i128) MINi8() <= (i128) i; (i128) i <= (i128) MAXi8();
-             (i128) MINi8() <= (i128) j; (i128) j <= (i128) MAXi8();
-             (i128) MINi8() <= (i128) k; (i128) k <= (i128) MAXi8();
-
-    ensures return == 0i32; @*/
+    requires  MINi32() <=  b;  b <=  MAXi32();
+
+              MINu8() <=  d;  d <=  MAXu8();
+              MINu8() <=  f;  f <=  MAXu8();
+              MINu8() <=  h;  h <=  MAXu8();
+              MINu8() <=  i;  i <=  MAXu8();
+              MINu8() <=  j;  j <=  MAXu8();
+
+              MINi8() <=  e;  e <=  MAXi8();
+              MINi8() <=  f;  f <=  MAXi8();
+              MINi8() <=  g;  g <=  MAXi8();
+              MINi8() <=  h;  h <=  MAXi8();
+              MINi8() <=  i;  i <=  MAXi8();
+              MINi8() <=  j;  j <=  MAXi8();
+              MINi8() <=  k;  k <=  MAXi8();
+
+    ensures return == 0; @*/
 {
 	a = b;
 	a = c;
diff --git a/src/example-archive/c-testsuite/working/00129.working.c b/src/example-archive/c-testsuite/working/00129.working.c
index b110e78e..36e24273 100644
--- a/src/example-archive/c-testsuite/working/00129.working.c
+++ b/src/example-archive/c-testsuite/working/00129.working.c
@@ -13,7 +13,7 @@ struct s {
 
 int
 main(void)
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 #undef s
 	goto s;
diff --git a/src/example-archive/c-testsuite/working/00134.c b/src/example-archive/c-testsuite/working/00134.c
index 75f70b78..00484afd 100644
--- a/src/example-archive/c-testsuite/working/00134.c
+++ b/src/example-archive/c-testsuite/working/00134.c
@@ -1,6 +1,6 @@
 int
 main(void)
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	long i;
 	unsigned long u;
diff --git a/src/example-archive/c-testsuite/working/00135.c b/src/example-archive/c-testsuite/working/00135.c
index 32eabbad..95942d38 100644
--- a/src/example-archive/c-testsuite/working/00135.c
+++ b/src/example-archive/c-testsuite/working/00135.c
@@ -2,7 +2,7 @@
 
 int
 main(void)
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	long long i;
 	unsigned long long u;
diff --git a/src/example-archive/c-testsuite/working/00136.working.c b/src/example-archive/c-testsuite/working/00136.working.c
index 504ba1fd..2b20919a 100644
--- a/src/example-archive/c-testsuite/working/00136.working.c
+++ b/src/example-archive/c-testsuite/working/00136.working.c
@@ -24,7 +24,7 @@
 	int f_;
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00139.working.c b/src/example-archive/c-testsuite/working/00139.working.c
index 4f50cf03..5842fd92 100644
--- a/src/example-archive/c-testsuite/working/00139.working.c
+++ b/src/example-archive/c-testsuite/working/00139.working.c
@@ -8,7 +8,7 @@
 
 int
 main(void)
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
         int f = 0;
 
diff --git a/src/example-archive/c-testsuite/working/00145.working.c b/src/example-archive/c-testsuite/working/00145.working.c
index e9daf49d..7db500ef 100644
--- a/src/example-archive/c-testsuite/working/00145.working.c
+++ b/src/example-archive/c-testsuite/working/00145.working.c
@@ -12,7 +12,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00146.working.c b/src/example-archive/c-testsuite/working/00146.working.c
index bfbd53a7..e180b4ed 100644
--- a/src/example-archive/c-testsuite/working/00146.working.c
+++ b/src/example-archive/c-testsuite/working/00146.working.c
@@ -5,9 +5,9 @@ int
 main()
 /*@ accesses s;
     requires 
-			s.a == 1i32; 
-			s.b == 2i32;
-    ensures return == 0i32; @*/
+			s.a == 1; 
+			s.b == 2;
+    ensures return == 0; @*/
 {
 	if(s.a != 1)
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00152.working.c b/src/example-archive/c-testsuite/working/00152.working.c
index 74c4fea1..676855fc 100644
--- a/src/example-archive/c-testsuite/working/00152.working.c
+++ b/src/example-archive/c-testsuite/working/00152.working.c
@@ -8,7 +8,7 @@
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	return 0;
 }
diff --git a/src/example-archive/c-testsuite/working/00153.working.c b/src/example-archive/c-testsuite/working/00153.working.c
index e7e57d02..fa04abf5 100644
--- a/src/example-archive/c-testsuite/working/00153.working.c
+++ b/src/example-archive/c-testsuite/working/00153.working.c
@@ -5,7 +5,7 @@ typedef struct { int f; } S;
 
 int
 main()
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	S s;
 
diff --git a/src/example-archive/c-testsuite/working/00155.working.c b/src/example-archive/c-testsuite/working/00155.working.c
index 2ecf6bf0..3633d35d 100644
--- a/src/example-archive/c-testsuite/working/00155.working.c
+++ b/src/example-archive/c-testsuite/working/00155.working.c
@@ -1,7 +1,7 @@
 
 int
 main(void)
-/*@ ensures return == 0i32; @*/
+/*@ ensures return == 0; @*/
 {
 	sizeof((int) 1);
 	return 0;
diff --git a/src/example-archive/dafny-tutorial/working/abs_1.c b/src/example-archive/dafny-tutorial/working/abs_1.c
index 1225c5c0..bbcc1546 100644
--- a/src/example-archive/dafny-tutorial/working/abs_1.c
+++ b/src/example-archive/dafny-tutorial/working/abs_1.c
@@ -1,10 +1,10 @@
 // Compute the absolute value a function.
 
 /*@
-function (i32) abs_spec(i32 x)
+function (integer) abs_spec(integer x)
 {
-  if (x < 0i32) {
-    (0i32 - x)
+  if (x < 0) {
+    (0 - x)
   } else {
     x
   }
@@ -13,13 +13,13 @@ function (i32) abs_spec(i32 x)
 
 int abs(int x)
 /*@ requires 
-      let MINi32 = (i64) -2147483647i64;
-      MINi32 < (i64) x;
+      let MINi32 = -2147483647;
+      MINi32 < x;
     ensures 
-      0i32 <= return; 
-      (x < 0i32 && return == (0i32 - x)) || (0i32 <= x && return == x); 
-      0i32 <= return && (return == x || return == (0i32 - x));  // Same property
-      return == abs_spec(x); @*/                                // Same property
+      0 <= return; 
+      (x < 0 && return == (0 - x)) || (0 <= x && return == x); 
+      0 <= return && (return == x || return == (0 - x));  // Same property
+      return == abs_spec(x); @*/                          // Same property
 {
   if (x < 0)
   {
@@ -34,6 +34,17 @@ int abs(int x)
 void abs_testing()
 {
   int v = abs(3);
+  #ifdef CN_INSTRUMENT
+  /*@ assert(0 <= v);
+      assert(v == 3); @*/
+  #else
   assert(0 <= v);
   assert(v == 3);
+  #endif
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  abs_testing();
+}
\ No newline at end of file
diff --git a/src/example-archive/dafny-tutorial/working/abs_2.c b/src/example-archive/dafny-tutorial/working/abs_2.c
index e1406d01..01d4c846 100644
--- a/src/example-archive/dafny-tutorial/working/abs_2.c
+++ b/src/example-archive/dafny-tutorial/working/abs_2.c
@@ -3,14 +3,19 @@
 
 int abs_2(int x)
 /*@ requires 
-      let MINi32 = (i64) -2147483647i64;
-
-      MINi32 <= (i64) x; 
-      x < 0i32;
+      let MINi32 = -2147483647;
+      MINi32 <= x; 
+      x < 0;
     ensures 
-      0i32 <= return; 
-      (return == x || return == (0i32 - x)); @*/
+      0 <= return; 
+      (return == x || return == (0 - x)); @*/
 {
   return -x;
 }
 
+int main(void)
+/*@ trusted; @*/
+{
+  int x = -42;
+  int abs_x = abs_2(x);
+}
\ No newline at end of file
diff --git a/src/example-archive/dafny-tutorial/working/abs_3.c b/src/example-archive/dafny-tutorial/working/abs_3.c
index f85490ef..0e34f456 100644
--- a/src/example-archive/dafny-tutorial/working/abs_3.c
+++ b/src/example-archive/dafny-tutorial/working/abs_3.c
@@ -3,11 +3,18 @@
 
 int abs_3(int x)
 /*@ requires 
-      x == (0i32 - 1i32);  // TODO: syntax is bad 
+      x == (0 - 1);  // TODO: syntax is bad 
     ensures 
-      0i32 <= return;
-      (return == x || return == (0i32 - x)); 
-      return == 1i32; @*/
+      0 <= return;
+      (return == x || return == (0 - x)); 
+      return == 1; @*/
 {
   return x + 2;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = -1;
+  int abs_x = abs_3(x);
+}
\ No newline at end of file
diff --git a/src/example-archive/dafny-tutorial/working/binary_search.c b/src/example-archive/dafny-tutorial/working/binary_search.c
index 0891241e..27fd2303 100644
--- a/src/example-archive/dafny-tutorial/working/binary_search.c
+++ b/src/example-archive/dafny-tutorial/working/binary_search.c
@@ -3,17 +3,17 @@
 
 int binary_search(int *a, int length, int value)
 /*@ requires 
-      let MAXi32 = (i64) 2147483647i64; // TODO: lift to library 
+      let MAXi32 = 2147483647; // TODO: lift to library 
 
-      0i32 <= length; 
-      (2i64 * (i64) length) <= MAXi32; 
-      take IndexPre = each (i32 j; 0i32 <= j && j < length)
+      0 <= length; 
+      (2 * length) <= MAXi32; 
+      take IndexPre = each (integer j; 0 <= j && j < length)
                            {RW<int>(a + j)};
     ensures 
-      take IndexPost = each (i32 j; 0i32 <= j && j < length)
+      take IndexPost = each (integer j; 0 <= j && j < length)
                             {RW<int>(a + j)}; 
       IndexPost == IndexPre; 
-      (return < 0i32) || (IndexPost[return] == value); @*/
+      (return < 0) || (IndexPost[return] == value); @*/
 {
   int low = 0;
   int high = length;
@@ -21,17 +21,17 @@ int binary_search(int *a, int length, int value)
   while (low < high)
   /*@ inv 
         {a}unchanged; {length}unchanged; {value}unchanged;  
-        0i32 <= low; 
+        0 <= low; 
         low <= high; 
         high <= length; 
-        ((i64) low + (i64) high) <= MAXi32; 
-        take IndexInv = each (i32 j; 0i32 <= j && j < length)
+        (low + high) <= MAXi32; 
+        take IndexInv = each (integer j; 0 <= j && j < length)
                              {RW<int>(a + j)}; 
         IndexInv == IndexPre; @*/
   {
     int mid = (low + high) / 2;
     /*@ focus RW<int>, mid; @*/
-    /*@ instantiate good<int>, mid;  @*/
+    /*@ instantiate mid;  @*/
     if (a[mid] < value)
     {
       low = mid + 1;
@@ -47,3 +47,10 @@ int binary_search(int *a, int length, int value)
   };
   return -1;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int xs[6] = {2,4,6,8,10,12};
+  binary_search(xs, 6, 12);
+}
\ No newline at end of file
diff --git a/src/example-archive/dafny-tutorial/working/linear_search.c b/src/example-archive/dafny-tutorial/working/linear_search.c
index 99cc9a65..3fe80f69 100644
--- a/src/example-archive/dafny-tutorial/working/linear_search.c
+++ b/src/example-archive/dafny-tutorial/working/linear_search.c
@@ -2,15 +2,15 @@
 
 int linear_search(int *a, int length, int key)
 /*@ requires 
-      0i32 < length; 
-      take IndexPre = each (i32 j; 0i32 <= j && j < length)
+      0 < length; 
+      take IndexPre = each (integer j; 0 <= j && j < length)
                            {RW<int>(a + j)};
     ensures 
-      take IndexPost = each (i32 j; 0i32 <= j && j < length)
+      take IndexPost = each (integer j; 0 <= j && j < length)
                             {RW<int>(a + j)};
-      (return < 0i32) || (IndexPost[return] == key); 
-      each (i32 j; 0i32 <= j && j < length) 
-           {return >= 0i32 || IndexPre[j] != key}; 
+      (return < 0) || (IndexPost[return] == key); 
+      each (integer j; 0 <= j && j < length) 
+           {return >= 0 || IndexPre[j] != key}; 
       IndexPre == IndexPost; @*/
 {
   int idx = 0;
@@ -18,14 +18,15 @@ int linear_search(int *a, int length, int key)
   while (idx < length)
   /*@ inv 
         {a}unchanged; {length}unchanged; {key}unchanged; 
-        0i32 <= idx; 
+        0 <= idx; 
         idx <= length; 
-        take IndexInv = each (i32 j; 0i32 <= j && j < length)
+        take IndexInv = each (integer j; 0 <= j && j < length)
                              {RW<int>(a + j)}; 
         IndexInv == IndexPre; 
-        each (i32 j; 0i32 <= j && j < idx) {IndexPre[j] != key}; @*/
+        each (integer j; 0 <= j && j < idx) {IndexPre[j] != key}; @*/
   {
     /*@ focus RW<int>, idx; @*/
+    /*@ instantiate idx; @*/
     if (*(a + idx) == key)
     {
       return idx;
@@ -36,3 +37,10 @@ int linear_search(int *a, int length, int key)
   return idx;
 }
 
+
+int main(void)
+/*@ trusted; @*/
+{
+  int xs[6] = {2,4,6,8,10,12};
+  linear_search(xs, 6, 12);
+}
\ No newline at end of file
diff --git a/src/example-archive/dafny-tutorial/working/max.c b/src/example-archive/dafny-tutorial/working/max.c
index f1d32d2a..59bd73dc 100644
--- a/src/example-archive/dafny-tutorial/working/max.c
+++ b/src/example-archive/dafny-tutorial/working/max.c
@@ -2,7 +2,7 @@
 // equivalent to the same algorithm implemented in the spec language 
 
 /*@
-function (i32) max_spec (i32 a, i32 b)
+function (integer) max_spec (integer a, integer b)
 {
   if (a > b){
     a
@@ -32,6 +32,15 @@ void max_test()
 {
   int v;
   v = max(-2, 7);
+  #ifdef CN_INSTRUMENT
+  /*@ assert (v == 7); @*/
+  #else
   assert(v == 7);
+  #endif
 }
 
+int main(void)
+/*@ trusted; @*/
+{
+  max_test();
+}
\ No newline at end of file
diff --git a/src/example-archive/dafny-tutorial/working/multiple_returns.c b/src/example-archive/dafny-tutorial/working/multiple_returns.c
index 662cfc97..ab220077 100644
--- a/src/example-archive/dafny-tutorial/working/multiple_returns.c
+++ b/src/example-archive/dafny-tutorial/working/multiple_returns.c
@@ -10,14 +10,14 @@ struct int_pair
 
 void multiple_returns(int x, int y, struct int_pair *ret)
 /*@ requires 
-      let MAXi32 = (i64) 2147483647i64; 
-      let MINi32 = (i64) -2147483647i64;
+      let MAXi32 = 2147483647; 
+      let MINi32 = -2147483647;
 
       take PairPre = RW<struct int_pair>(ret);
-      MINi32 <= (i64) x + (i64) y; 
-      (i64) x + (i64) y <= MAXi32;
-      MINi32 <= (i64) x - (i64) y; 
-      (i64) x - (i64) y <= MAXi32;
+      MINi32 <= x + y; 
+      x + y <= MAXi32;
+      MINi32 <= x - y; 
+      x - y <= MAXi32;
     ensures 
       take PairPost = RW<struct int_pair>(ret);
       PairPost.fst == x + y;
@@ -27,3 +27,12 @@ void multiple_returns(int x, int y, struct int_pair *ret)
   ret->snd = x - y;
   return;
 }
+
+void *cn_malloc(unsigned long size);
+
+int main(void)
+/*@ trusted; @*/
+{
+  struct int_pair *is = cn_malloc(sizeof(struct int_pair));
+  multiple_returns(10, 100, is);
+}
\ No newline at end of file
diff --git a/src/example-archive/java_program_verification_challenges/broken/error-proof/00006_callbacks.c b/src/example-archive/java_program_verification_challenges/broken/error-proof/00006_callbacks.c
index b9ccdb78..3c177033 100644
--- a/src/example-archive/java_program_verification_challenges/broken/error-proof/00006_callbacks.c
+++ b/src/example-archive/java_program_verification_challenges/broken/error-proof/00006_callbacks.c
@@ -73,13 +73,13 @@ struct A {
  */
 void decrement_k(A *a)
   /*@ requires take va0 = RW<A>(a);
-               va0.m < 2147483647i32;
-               -2147483648i32 < va0.k;
-	       va0.k + va0.m == 0i32
+               va0.m < 2147483647;
+               -2147483648 < va0.k;
+	       va0.k + va0.m == 0
       ensures take va1 = RW<A>(a);
-              va1.k == va0.k-1i32;
-              va1.m == va0.m+1i32;
-	      va1.k + va1.m == 0i32
+              va1.k == va0.k-1;
+              va1.m == va0.m+1;
+	      va1.k + va1.m == 0
   @*/
 {
     a->k--;
@@ -98,14 +98,14 @@ void decrement_k(A *a)
  */
 void increment_k(A *a)
   /*@ requires take va0 = RW<A>(a);
-               va0.k < 2147483647i32;
-               va0.m < 2147483647i32;
-               -2147483648i32 < va0.m;
-	       va0.k + va0.m == 0i32
+               va0.k < 2147483647;
+               va0.m < 2147483647;
+               -2147483648 < va0.m;
+	       va0.k + va0.m == 0
       ensures take va1 = RW<A>(a);
               va1.k == va0.k;
               va1.m == va0.m;
-	      va1.k + va1.m == 0i32
+	      va1.k + va1.m == 0
   @*/
 {
     a->k++;
diff --git a/src/example-archive/java_program_verification_challenges/broken/error-proof/00011_dependen_specifications.c b/src/example-archive/java_program_verification_challenges/broken/error-proof/00011_dependen_specifications.c
index 3931de74..8e609c06 100644
--- a/src/example-archive/java_program_verification_challenges/broken/error-proof/00011_dependen_specifications.c
+++ b/src/example-archive/java_program_verification_challenges/broken/error-proof/00011_dependen_specifications.c
@@ -61,7 +61,7 @@ int iabs(int x)
  *          x < (iabs(\result) + 1) * (iabs(\result) + 1);
  */
 int isqrt(int x)
-  /*@ requires 0i32 <= x ; x<= 2147390966i32; 
+  /*@ requires 0 <= x ; x<= 2147390966; 
       ensures true; 
   @*/
 {
@@ -74,11 +74,11 @@ int isqrt(int x)
      * @ decreasing x - count;
      */
     while (sum <= x)
-    /*@ inv 0i32 <= count;
-            count < 46340i32;
+    /*@ inv 0 <= count;
+            count < 46340;
 	    count * count <= x;
-	    sum == (count + 1i32 ) * (count + 1i32);
-	    sum <= x + 2i32 *count+1i32; 
+	    sum == (count + 1 ) * (count + 1);
+	    sum <= x + 2 *count+1; 
       @*/
     {
         count++;
diff --git a/src/example-archive/java_program_verification_challenges/working/00004_exceptions.c b/src/example-archive/java_program_verification_challenges/working/00004_exceptions.c
index 1fda6ff0..c54cc1f6 100644
--- a/src/example-archive/java_program_verification_challenges/working/00004_exceptions.c
+++ b/src/example-archive/java_program_verification_challenges/working/00004_exceptions.c
@@ -39,8 +39,9 @@ int m; // Global variable m
  */
 int returnfinally(int d)
   /*@ requires take vp0 = RW<int>(&m);
-               let m10 = (i64)vp0 + 10i64;
-               m10 <= 2147483647i64; 
+               let m10 = vp0 + 10;
+               m10 <= 2147483647; 
+	       MINi32() <= vp0/d && vp0/d <= MAXi32();  // CP: added
       ensures take vp1 = RW<int>(&m); 
   @*/
   {
@@ -60,7 +61,7 @@ int returnfinally(int d)
 int main()
   /*@ requires take vp0 = RW<int>(&m); 
       ensures take vp1 = W<int>(&m);
-	      return == 0i32; 
+	      return == 0; 
   @*/
 {
     m = 20; // Initialize m
diff --git a/src/example-archive/open-sut/working/mps_1.c b/src/example-archive/open-sut/broken/error-proof/mps_1.c
similarity index 62%
rename from src/example-archive/open-sut/working/mps_1.c
rename to src/example-archive/open-sut/broken/error-proof/mps_1.c
index a26919c0..b193994b 100644
--- a/src/example-archive/open-sut/working/mps_1.c
+++ b/src/example-archive/open-sut/broken/error-proof/mps_1.c
@@ -23,11 +23,11 @@ typedef uint8_t w8;
     (a&&b) || ((a||b) && (c||d)) || (c&&d)
   }
 
-  function (u8) Bool_to_u8(boolean b) {
+  function (integer) Bool_to_u8(boolean b) {
     if(b) {
-      1u8
+      1
     } else {
-      0u8
+      0
     }
   }
 @*/
@@ -35,19 +35,19 @@ typedef uint8_t w8;
 w1 Coincidence_2_4(w8 trips[4])
 /*@
   requires
-    take ta = RW<uint8_t>(array_shift<uint8_t>(trips, 0i32));
-    take tb = RW<uint8_t>(array_shift<uint8_t>(trips, 1i32));
-    take tc = RW<uint8_t>(array_shift<uint8_t>(trips, 2i32));
-    take td = RW<uint8_t>(array_shift<uint8_t>(trips, 3i32));
-    let a = ta != 0u8;
-    let b = tb != 0u8;
-    let c = tc != 0u8;
-    let d = td != 0u8;
+    take ta = RW<uint8_t>(array_shift<uint8_t>(trips, 0));
+    take tb = RW<uint8_t>(array_shift<uint8_t>(trips, 1));
+    take tc = RW<uint8_t>(array_shift<uint8_t>(trips, 2));
+    take td = RW<uint8_t>(array_shift<uint8_t>(trips, 3));
+    let a = ta != 0;
+    let b = tb != 0;
+    let c = tc != 0;
+    let d = td != 0;
   ensures
-    take ta_out = RW<uint8_t>(array_shift<uint8_t>(trips, 0i32));
-    take tb_out = RW<uint8_t>(array_shift<uint8_t>(trips, 1i32));
-    take tc_out = RW<uint8_t>(array_shift<uint8_t>(trips, 2i32));
-    take td_out = RW<uint8_t>(array_shift<uint8_t>(trips, 3i32));
+    take ta_out = RW<uint8_t>(array_shift<uint8_t>(trips, 0));
+    take tb_out = RW<uint8_t>(array_shift<uint8_t>(trips, 1));
+    take tc_out = RW<uint8_t>(array_shift<uint8_t>(trips, 2));
+    take td_out = RW<uint8_t>(array_shift<uint8_t>(trips, 3));
     return == Bool_to_u8(P_Coincidence_2_4(a, b, c, d));
 @*/
 {
diff --git a/src/example-archive/runtime-extras/bad_free.broken.c b/src/example-archive/runtime-extras/bad_free.broken.c
new file mode 100644
index 00000000..16523f05
--- /dev/null
+++ b/src/example-archive/runtime-extras/bad_free.broken.c
@@ -0,0 +1,25 @@
+#ifndef CN_UTILS
+#include <stdlib.h>
+void *cn_malloc(unsigned long size);
+void cn_free_sized(void* p, unsigned long s);
+#endif
+
+int *malloc_int()
+/*@ trusted;
+    ensures take X = Block<int>(return); @*/
+{
+    return cn_malloc(sizeof(int));
+}
+
+void bad_free(int *p)
+/*@ trusted; @*/
+{
+    cn_free_sized(p, sizeof(int));
+}
+
+int main()
+/*@ trusted; @*/
+{
+    int *p = malloc_int();
+    bad_free(p);
+}
diff --git a/src/example-archive/runtime-extras/double_free.broken.c b/src/example-archive/runtime-extras/double_free.broken.c
new file mode 100644
index 00000000..746bf6ee
--- /dev/null
+++ b/src/example-archive/runtime-extras/double_free.broken.c
@@ -0,0 +1,31 @@
+#ifndef CN_UTILS
+#include <stdlib.h>
+void *cn_malloc(unsigned long size);
+void cn_free_sized(void* p, unsigned long s);
+#endif
+
+unsigned int deref(unsigned int *p)
+/*@ trusted;
+requires
+    take v1_ = Owned(p);
+ensures
+    take v2 = Owned(p);
+    v1_ == v2;
+    return == v1_;
+@*/
+{
+  return *p;
+}
+
+int main()
+/*@ trusted; @*/
+{
+    unsigned int *p = cn_malloc(sizeof(unsigned int));
+    *p = 5;
+    unsigned int x = deref(p);
+    /*@ assert (x == 5u32); @*/
+    /*@ assert (*p == 5u32); @*/
+    cn_free_sized(p, sizeof(unsigned int));
+    // double free
+    cn_free_sized(p, sizeof(unsigned int));
+}
diff --git a/src/example-archive/runtime-extras/down_malloc_up_free.c b/src/example-archive/runtime-extras/down_malloc_up_free.c
new file mode 100644
index 00000000..ac21bd66
--- /dev/null
+++ b/src/example-archive/runtime-extras/down_malloc_up_free.c
@@ -0,0 +1,27 @@
+#ifndef CN_UTILS
+#include <stdlib.h>
+void *cn_malloc(unsigned long size);
+void cn_free_sized(void* p, unsigned long s);
+#endif
+
+unsigned int read_and_free(unsigned int *p)
+/*@ trusted;
+requires
+    take v1_ = Owned(p);
+ensures
+    return == v1_;
+@*/
+{
+  unsigned int result = *p;
+  cn_free_sized(p, sizeof(unsigned int));
+  return result;
+}
+
+int main()
+/*@ trusted; @*/
+{
+    unsigned int *x = cn_malloc(sizeof(unsigned int));
+    *x = 5;
+    unsigned int res = read_and_free(x);
+    /*@ assert (res == 5); @*/
+}
diff --git a/src/example-archive/runtime-extras/leaky.broken.c b/src/example-archive/runtime-extras/leaky.broken.c
new file mode 100644
index 00000000..e707d4d1
--- /dev/null
+++ b/src/example-archive/runtime-extras/leaky.broken.c
@@ -0,0 +1,24 @@
+#ifndef CN_UTILS
+#include <stdlib.h>
+void *cn_malloc(unsigned long size);
+void cn_free_sized(void* p, unsigned long s);
+#endif
+
+unsigned int leaky_get (unsigned int *p)
+/*@ trusted;
+requires
+    take v1_ = Owned(p);
+ensures
+    return == v1_;
+@*/
+{
+  return *p;
+}
+
+int main()
+/*@ trusted; @*/
+{
+    unsigned int *x = cn_malloc(sizeof(unsigned int));
+    *x = 5;
+    unsigned int res = leaky_get(x);
+}
diff --git a/src/example-archive/runtime-extras/leaky_main.c b/src/example-archive/runtime-extras/leaky_main.c
new file mode 100644
index 00000000..4e70faf8
--- /dev/null
+++ b/src/example-archive/runtime-extras/leaky_main.c
@@ -0,0 +1,28 @@
+#ifndef CN_UTILS
+#include <stdlib.h>
+void *cn_malloc(unsigned long size);
+void cn_free_sized(void* p, unsigned long s);
+#endif
+
+unsigned int *mkref(unsigned int x)
+/*@ trusted;
+requires
+    true;
+ensures
+    take v1_ = Owned(return);
+    v1_ == x;
+@*/
+{
+  unsigned int *p = cn_malloc(sizeof(unsigned int));
+  *p = x;
+  return p;
+}
+
+int main()
+/*@ trusted; @*/
+{
+    unsigned int *p = mkref(5);
+    /*@ assert (*p == 5u32); @*/
+    // TODO - consider decrementing stack-depth for main too?
+    // or it doesn't matter? main can be called multiple times.
+}
diff --git a/src/example-archive/runtime-extras/return_owned_local.broken.c b/src/example-archive/runtime-extras/return_owned_local.broken.c
new file mode 100644
index 00000000..c51c011f
--- /dev/null
+++ b/src/example-archive/runtime-extras/return_owned_local.broken.c
@@ -0,0 +1,45 @@
+#ifndef CN_UTILS
+#include <stdlib.h>
+void *cn_malloc(unsigned long size);
+void cn_free_sized(void* p, unsigned long s);
+#endif
+
+unsigned int get (unsigned int *p)
+/*@
+requires
+    take v1_ = Owned(p);
+ensures
+    take v2 = Owned(p);
+    v2 == v1_; return == v1_;
+@*/
+{
+  return *p;
+}
+
+
+unsigned int **bad(unsigned int *p)
+/*@ trusted;
+requires
+    take v1_ = Owned(p);
+ensures
+    take v2 = Owned(p);
+    take p2 = Owned(return);
+    ptr_eq(p, p2);
+    v1_ == v2;
+@*/
+{
+    return &p;
+}
+
+int main()
+/*@ trusted; @*/
+{
+    unsigned int *x = cn_malloc(sizeof(unsigned int));
+    *x = 5;
+    unsigned int res = get(x);
+    /*@ assert (res == 5u32); @*/
+    *x = 6;
+    /*@ assert (*x == 6u32); @*/
+
+    unsigned int **p = bad(x);
+}
diff --git a/src/example-archive/runtime-extras/same_func_malloc_free.c b/src/example-archive/runtime-extras/same_func_malloc_free.c
new file mode 100644
index 00000000..4b04a433
--- /dev/null
+++ b/src/example-archive/runtime-extras/same_func_malloc_free.c
@@ -0,0 +1,29 @@
+#ifndef CN_UTILS
+#include <stdlib.h>
+void *cn_malloc(unsigned long size);
+void cn_free_sized(void* p, unsigned long s);
+#endif
+
+unsigned int deref(unsigned int *p)
+/*@ trusted;
+requires
+    take v1_ = Owned(p);
+ensures
+    take v2 = Owned(p);
+    v1_ == v2;
+    return == v1_;
+@*/
+{
+  return *p;
+}
+
+int main()
+/*@ trusted; @*/
+{
+    unsigned int *p = cn_malloc(sizeof(unsigned int));
+    *p = 5;
+    unsigned int x = deref(p);
+    /*@ assert (x == 5u32); @*/
+    /*@ assert (*p == 5u32); @*/
+    cn_free_sized(p, sizeof(unsigned int));
+}
diff --git a/src/example-archive/runtime-extras/swap_array.c b/src/example-archive/runtime-extras/swap_array.c
new file mode 100644
index 00000000..ea37ad67
--- /dev/null
+++ b/src/example-archive/runtime-extras/swap_array.c
@@ -0,0 +1,36 @@
+void swap_array (int *p, int n, int i, int j)
+/* --BEGIN-- */
+/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned<int>(array_shift<int>(p,k)) };
+             0i32 <= i && i < n;
+             0i32 <= j && j < n;
+             j != i;
+    ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned<int>(array_shift<int>(p,k)) };
+            a2 == a1[i: a1[j], j: a1[i]];
+@*/
+/* --END-- */
+{
+/* --BEGIN-- */
+  /*@ extract Owned<int>, i; @*/
+/* --END-- */
+  int tmp = p[i];
+/* --BEGIN-- */
+  /*@ extract Owned<int>, j; @*/
+/* --END-- */
+  p[i] = p[j];
+  p[j] = tmp;
+}
+
+int main()
+/*@ trusted; @*/
+{
+    int a[3] = { 0, 1, 2 };
+
+    swap_array(a, 3, 0, 2);
+    int *first = a;
+    int *third = a + 2;
+    /*@ assert (*third == 0i32); @*/
+    /*@ assert (*first == 2i32); @*/
+
+    // uncomment for failure
+    // swap_array(a, 3, 1, 1);
+}
diff --git a/src/example-archive/runtime-extras/up_malloc_down_free.c b/src/example-archive/runtime-extras/up_malloc_down_free.c
new file mode 100644
index 00000000..98b33ad2
--- /dev/null
+++ b/src/example-archive/runtime-extras/up_malloc_down_free.c
@@ -0,0 +1,27 @@
+#ifndef CN_UTILS
+#include <stdlib.h>
+void *cn_malloc(unsigned long size);
+void cn_free_sized(void* p, unsigned long s);
+#endif
+
+unsigned int *mkref(unsigned int x)
+/*@ trusted;
+requires
+    true;
+ensures
+    take v1_ = Owned(return);
+    v1_ == x;
+@*/
+{
+  unsigned int *p = cn_malloc(sizeof(unsigned int));
+  *p = x;
+  return p;
+}
+
+int main()
+/*@ trusted; @*/
+{
+    unsigned int *p = mkref(5);
+    /*@ assert (*p == 5u32); @*/
+    cn_free_sized(p, sizeof(unsigned int));
+}
diff --git a/src/example-archive/should-fail/broken/error-proof/arith_neg_1.c b/src/example-archive/should-fail/broken/error-proof/arith_neg_1.c
index 01ef29d6..a694b05a 100644
--- a/src/example-archive/should-fail/broken/error-proof/arith_neg_1.c
+++ b/src/example-archive/should-fail/broken/error-proof/arith_neg_1.c
@@ -3,7 +3,14 @@
 // The specification claims the function returns a non-zero value, but the
 // implementation returns zero.
 int arith_neg_1() 
-/*@ ensures return != 0i32; @*/
+/*@ ensures return != 0; @*/
 {
   return 0; 
+}
+
+
+int main(void)
+/*@ trusted; @*/
+{
+  arith_neg_1();
 }
\ No newline at end of file
diff --git a/src/example-archive/should-fail/broken/error-proof/memory_neg_1.c b/src/example-archive/should-fail/broken/error-proof/memory_neg_1.c
index 1e22d86c..654b9921 100644
--- a/src/example-archive/should-fail/broken/error-proof/memory_neg_1.c
+++ b/src/example-archive/should-fail/broken/error-proof/memory_neg_1.c
@@ -5,4 +5,11 @@
 void memory_neg_1( int *p )
 {
   *p = 1; 
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 42;
+  memory_neg_1(&x);
 }
\ No newline at end of file
diff --git a/src/example-archive/should-fail/broken/error-proof/overflow_neg_1.c b/src/example-archive/should-fail/broken/error-proof/overflow_neg_1.c
index f3a4088a..b0e04b72 100644
--- a/src/example-archive/should-fail/broken/error-proof/overflow_neg_1.c
+++ b/src/example-archive/should-fail/broken/error-proof/overflow_neg_1.c
@@ -7,3 +7,10 @@ void overflow_neg_1(int i)
 {
   i = i + 1; 
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 2147483647;
+  overflow_neg_1(x);
+}
diff --git a/src/example-archive/should-fail/broken/error-proof/overflow_neg_2.c b/src/example-archive/should-fail/broken/error-proof/overflow_neg_2.c
index 3542e353..f6f82f09 100644
--- a/src/example-archive/should-fail/broken/error-proof/overflow_neg_2.c
+++ b/src/example-archive/should-fail/broken/error-proof/overflow_neg_2.c
@@ -6,4 +6,11 @@ void overflow_neg_2(int i)
 /*@ requires i == MINi32(); @*/
 {
   i = i - 1; 
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = -2147483648;
+  overflow_neg_2(x);
 }
\ No newline at end of file
diff --git a/src/example-archive/should-fail/broken/error-proof/ownership_neg_1.c b/src/example-archive/should-fail/broken/error-proof/ownership_neg_1.c
index 2903b829..194223fa 100644
--- a/src/example-archive/should-fail/broken/error-proof/ownership_neg_1.c
+++ b/src/example-archive/should-fail/broken/error-proof/ownership_neg_1.c
@@ -3,8 +3,15 @@
 // Precondition includes access to the resource RW(p), which disappears in
 // the postcondition 
 void ownership_neg_1(int *p) 
-/*@ requires take P = RW(p); @*/
-/*@ ensures true; @*/
+/*@ requires take P = RW(p);
+    ensures true; @*/
 {
   ; 
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 42;
+  ownership_neg_1(&x);
 }
\ No newline at end of file
diff --git a/src/example-archive/should-fail/broken/error-proof/ownership_neg_2.c b/src/example-archive/should-fail/broken/error-proof/ownership_neg_2.c
index b375b5d7..1308adeb 100644
--- a/src/example-archive/should-fail/broken/error-proof/ownership_neg_2.c
+++ b/src/example-archive/should-fail/broken/error-proof/ownership_neg_2.c
@@ -3,8 +3,15 @@
 // Precondition takes ownership of no resources, but then the postcondition
 // claims ownership of RW(p)  
 void ownership_neg_2(int *p) 
-/*@ requires true; @*/
-/*@ ensures take P_ = RW(p); @*/
+/*@ requires true; 
+    ensures take P_ = RW(p); @*/
 {
   ; 
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 42;
+  ownership_neg_2(&x);
 }
\ No newline at end of file
diff --git a/src/example-archive/should-fail/broken/error-proof/ownership_neg_3.c b/src/example-archive/should-fail/broken/error-proof/ownership_neg_3.c
index 4a0fba43..b8a8af77 100644
--- a/src/example-archive/should-fail/broken/error-proof/ownership_neg_3.c
+++ b/src/example-archive/should-fail/broken/error-proof/ownership_neg_3.c
@@ -3,10 +3,17 @@
 // Precondition includes access to the resource RW(p), which is duplicated in
 // the postcondition  
 void ownership_neg_3(int *p) 
-/*@ requires take P = RW(p); @*/
-/*@ ensures 
+/*@ requires take P = RW(p);
+    ensures 
       take P_ = RW(p); 
       take Q_ = RW(p); @*/
 {
   ; 
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 42;
+  ownership_neg_3(&x);
 }
\ No newline at end of file
diff --git a/src/example-archive/should-fail/broken/error-proof/trivial_neg_1.c b/src/example-archive/should-fail/broken/error-proof/trivial_neg_1.c
index 4ef975bf..3d2e80d5 100644
--- a/src/example-archive/should-fail/broken/error-proof/trivial_neg_1.c
+++ b/src/example-archive/should-fail/broken/error-proof/trivial_neg_1.c
@@ -5,4 +5,10 @@ void trivial_neg_1()
 /*@ ensures false; @*/
 {
   ; 
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  trivial_neg_1();
 }
\ No newline at end of file
diff --git a/src/example-archive/should-fail/working/c_sequencing_race.c b/src/example-archive/should-fail/working/c_sequencing_race.c
index 8b6a0b1f..0b7ade44 100644
--- a/src/example-archive/should-fail/working/c_sequencing_race.c
+++ b/src/example-archive/should-fail/working/c_sequencing_race.c
@@ -3,8 +3,15 @@
 int
 f (int *x)
 /*@ requires take xv = RW(x);
-             0i32 <= xv && xv < 500i32;
+             0 <= xv && xv < 500;
     ensures take xv2 = RW(x); @*/
 {
   return ((*x) + (*x));
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int y = 12;
+  f(&y);
+}
\ No newline at end of file
diff --git a/src/example-archive/should-fail/working/letweak01.c b/src/example-archive/should-fail/working/letweak01.c
index be7d7fd6..51382a76 100644
--- a/src/example-archive/should-fail/working/letweak01.c
+++ b/src/example-archive/should-fail/working/letweak01.c
@@ -6,3 +6,8 @@ f (int x) {
   return x + 2;
 }
 
+int main(void)
+/*@ trusted; @*/
+{
+  f(406);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/broken/error-timeout/case_timeout.c b/src/example-archive/simple-examples/broken/error-proof/case_timeout.c
similarity index 87%
rename from src/example-archive/simple-examples/broken/error-timeout/case_timeout.c
rename to src/example-archive/simple-examples/broken/error-proof/case_timeout.c
index 4238f9a2..489dab4e 100644
--- a/src/example-archive/simple-examples/broken/error-timeout/case_timeout.c
+++ b/src/example-archive/simple-examples/broken/error-proof/case_timeout.c
@@ -19,4 +19,10 @@ int case_timeout(int a, int b){
     return a*b;
   }
   return 0;
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+    case_timeout(5, 10);
 }
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/cn_function_1.c b/src/example-archive/simple-examples/broken/error-proof/cn_function_1.c
similarity index 92%
rename from src/example-archive/simple-examples/working/cn_function_1.c
rename to src/example-archive/simple-examples/broken/error-proof/cn_function_1.c
index dd1250b7..4b4d8b45 100644
--- a/src/example-archive/simple-examples/working/cn_function_1.c
+++ b/src/example-archive/simple-examples/broken/error-proof/cn_function_1.c
@@ -3,7 +3,7 @@
 
 // Give the CN-level signature for bitwise-OR 
 /*@
-function (i32) bw_or(i32 x, i32 y)
+function (integer) bw_or(integer x, integer y)
 @*/
 
 // Define bitwise-OR in code
diff --git a/src/example-archive/simple-examples/working/cn_function_2.c b/src/example-archive/simple-examples/broken/error-proof/cn_function_2.c
similarity index 90%
rename from src/example-archive/simple-examples/working/cn_function_2.c
rename to src/example-archive/simple-examples/broken/error-proof/cn_function_2.c
index 76c73c67..5123d124 100644
--- a/src/example-archive/simple-examples/working/cn_function_2.c
+++ b/src/example-archive/simple-examples/broken/error-proof/cn_function_2.c
@@ -2,7 +2,7 @@
 
 // Give the CN-level signature for bitwise-OR 
 /*@
-function (i32) bw_or_tern(i32 x, i32 y, i32 z)
+function (integer) bw_or_tern(integer x, integer y, integer z)
 @*/
 
 // Define bitwise-OR in code
diff --git a/src/example-archive/simple-examples/broken/error-proof/loop_4.c b/src/example-archive/simple-examples/broken/error-proof/loop_4.c
index d8fc8a77..497ac3c2 100644
--- a/src/example-archive/simple-examples/broken/error-proof/loop_4.c
+++ b/src/example-archive/simple-examples/broken/error-proof/loop_4.c
@@ -44,3 +44,10 @@ void loop_4_with_redundant_write ()
   }
 }
 
+int main(void)
+/*@ trusted; @*/
+{
+  loop_4();
+  loop_4_unrolled();
+  loop_4_with_redundant_write();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/broken/error-proof/ownership_1.c b/src/example-archive/simple-examples/broken/error-proof/ownership_1.c
index d8bdaba1..aa834a86 100644
--- a/src/example-archive/simple-examples/broken/error-proof/ownership_1.c
+++ b/src/example-archive/simple-examples/broken/error-proof/ownership_1.c
@@ -9,8 +9,17 @@ requires
   take P2 = RW(b);
 ensures 
   a != b; 
+  take P1_ = RW(a); 
+  take P2_ = RW(b);
 @*/
 {
   /*@ split_case a == b; @*/
   ; 
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 10, y = 42;
+  ownership_1(&x, &y);
 }
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c b/src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c
index 1b59c111..756e7e12 100644
--- a/src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c
+++ b/src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c
@@ -7,3 +7,10 @@ pointerdec_crash_3()
   int *p = &arr[1];
   *(--p); 
 }
+
+
+int main(void)
+/*@ trusted; @*/
+{
+  pointerdec_crash_3();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/broken/error-proof/self_ref_init.c b/src/example-archive/simple-examples/broken/error-proof/self_ref_init.c
index 6195b3c9..52427370 100644
--- a/src/example-archive/simple-examples/broken/error-proof/self_ref_init.c
+++ b/src/example-archive/simple-examples/broken/error-proof/self_ref_init.c
@@ -7,7 +7,7 @@ struct str {
 };
 
 int f (int x)
-/*@ requires (0i32 <= x) && (x < 200i32); @*/
+/*@ requires (0 <= x) && (x < 200); @*/
 {
   struct str str_inst = {
     .x = x + 2,
@@ -17,3 +17,8 @@ int f (int x)
   return str_inst.y;
 }
 
+int main(void)
+/*@ trusted; @*/
+{
+  int r = f(42);
+}
diff --git a/src/example-archive/simple-examples/broken/error-proof/shift_crash_1.c b/src/example-archive/simple-examples/broken/error-proof/shift_crash_1.c
index 4352e794..37b4fbc3 100644
--- a/src/example-archive/simple-examples/broken/error-proof/shift_crash_1.c
+++ b/src/example-archive/simple-examples/broken/error-proof/shift_crash_1.c
@@ -3,3 +3,9 @@
 
 #include <stdint.h>
 uint8_t a(uint32_t b, uint32_t c, uint8_t ch) { a(b, c, 1) << 1; }
+
+int main(void)
+/*@ trusted; @*/
+{
+    a(1,2,3);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/broken/error-timeout/mult_timeout.c b/src/example-archive/simple-examples/broken/error-timeout/mult_timeout.c
deleted file mode 100644
index cf3185c3..00000000
--- a/src/example-archive/simple-examples/broken/error-timeout/mult_timeout.c
+++ /dev/null
@@ -1,10 +0,0 @@
-// Filed by @lwli11, see https://github.com/rems-project/cerberus/issues/856
-
-#include <limits.h>
-
-int mult_timeout(int a, int b){
-  if (a > 0 && b>0 && INT_MAX / b > a){
-    return a*b;
-  }
-  return 0;
-}
diff --git a/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c.skip b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c.skip
index 1b8ef064..9f0dd63d 100644
--- a/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c.skip
+++ b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c.skip
@@ -4,7 +4,7 @@
 
 extern int pow(int a, int b);
 /*@
-        spec pow(i32 a, i32 b);
+        spec pow(integer a, integer b);
         requires true;
         ensures true;
 @*/
diff --git a/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c
index a7b787ab..33696c8e 100644
--- a/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c
+++ b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c
@@ -4,7 +4,7 @@
 
 extern int pow(int a, int b);
 /*@
-        spec pow(i32 a, i32 b);
+        spec pow(integer a, integer b);
         requires true;
         ensures true;
 @*/
@@ -69,3 +69,16 @@ int overflow_timeout_4var(example_t* p1,example_t* p2)
         return distance;
 
 }
+
+void* cn_malloc(unsigned long size);
+
+int main(void)
+/*@ trusted; @*/
+{
+  example_t *p1 = cn_malloc(sizeof(example_t));
+  p1->x = 1; p1->y = 4; p1->z = 9; p1->a = 5; p1->b = 7;
+  example_t *p2 = cn_malloc(sizeof(example_t));
+  p2->x = 3; p2->y = 4; p2->z = 7; p2->a = 1; p2->b = 3;
+
+  int r = overflow_timeout_4var(p1, p2);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/inprogress/power_3.c b/src/example-archive/simple-examples/inprogress/power_3.c
index dd178cab..35789cc9 100644
--- a/src/example-archive/simple-examples/inprogress/power_3.c
+++ b/src/example-archive/simple-examples/inprogress/power_3.c
@@ -2,38 +2,38 @@
 // TODO: fix this 
 
 /*@
-lemma LemmaPowerUFDef(i32 i)
+lemma LemmaPowerUFDef(integer i)
   requires 
-    0i32 <= i
+    0 <= i
   ensures 
-    power_uf(2i32,0i32) == 1i32; 
-    power_uf(2i32,i+1i32) == (power_uf(2i32,i) * 2i32)
+    power_uf(2,0) == 1; 
+    power_uf(2,i+1) == (power_uf(2,i) * 2)
 @*/
 
 /*@
-lemma LemmaPowerOrd(i32 i, i32 j)
+lemma LemmaPowerOrd(integer i, integer j)
   requires
-    0i32 <= i;
+    0 <= i;
     i < j
   ensures 
-    (power_uf(2i32, i) * 2i32) <= power_uf(2i32,j)
+    (power_uf(2, i) * 2) <= power_uf(2,j)
 @*/
 
 int power2_3(int y)
 /*@ requires 
-      let MAXi32 = 2147483647i64; 
-      0i32 < y; 
-      (i64) power_uf(2i32,y) <= MAXi32 @*/
-/*@ ensures return == power_uf(2i32,y) @*/
+      let MAXi32 = 2147483647; 
+      0 < y; 
+      power_uf(2,y) <= MAXi32 @*/
+/*@ ensures return == power_uf(2,y) @*/
 {
     int i = 0;
     int pow = 1;
     /*@ apply LemmaPowerUFDef(i); @*/
 
     while (i < y)
-    /*@ inv 0i32 <= i; i <= y;
+    /*@ inv 0 <= i; i <= y;
             {y}unchanged; 
-            pow == power_uf(2i32,i) @*/
+            pow == power_uf(2,i) @*/
     {
         /*@ apply LemmaPowerUFDef(i); @*/
         /*@ apply LemmaPowerOrd(i,y); @*/
diff --git a/src/example-archive/simple-examples/working/add_1.c b/src/example-archive/simple-examples/working/add_1.c
index d774c53b..205b94a2 100644
--- a/src/example-archive/simple-examples/working/add_1.c
+++ b/src/example-archive/simple-examples/working/add_1.c
@@ -3,10 +3,16 @@
 // non-faulting.
 
 signed int add_1(signed int x, signed int y)
-/*@ requires x == 0i32; y == 0i32;
+/*@ requires x == 0; y == 0;
     ensures return == x + y; @*/
 {
   signed int i;
   i = x + y;
   return i;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  signed int r = add_1(0, 0);
+}
diff --git a/src/example-archive/simple-examples/working/add_2.c b/src/example-archive/simple-examples/working/add_2.c
index a0024aef..cbe0edad 100644
--- a/src/example-archive/simple-examples/working/add_2.c
+++ b/src/example-archive/simple-examples/working/add_2.c
@@ -2,10 +2,16 @@
 // requires-clause sets one integer to be zero 
 
 signed int add_2(signed int x, signed int y)
-/*@ requires x == 0i32;
+/*@ requires x == 0;
     ensures return == y; @*/
 {
   signed int i;
   i = x + y;
   return i;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  signed int r = add_2(0, 33);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/add_3.c b/src/example-archive/simple-examples/working/add_3.c
index f8dde358..96ce2877 100644
--- a/src/example-archive/simple-examples/working/add_3.c
+++ b/src/example-archive/simple-examples/working/add_3.c
@@ -3,9 +3,9 @@
 
 signed int add_3(signed int x, signed int y)
 /*@ requires 
-      let MAXi32 = 2147483647i64; 
-      let MINi32 = -2147483648i64;
-      let sum = (i64) x + (i64) y;
+      let MAXi32 = 2147483647; 
+      let MINi32 = -2147483648;
+      let sum = x + y;
       MINi32 <= sum; sum <= MAXi32;
     ensures return == x + y; @*/
 {
@@ -13,3 +13,9 @@ signed int add_3(signed int x, signed int y)
   i = x + y;
   return i;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  signed int r = add_3(500, 504);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/add_4.c b/src/example-archive/simple-examples/working/add_4.c
index 841908d5..fb8a2399 100644
--- a/src/example-archive/simple-examples/working/add_4.c
+++ b/src/example-archive/simple-examples/working/add_4.c
@@ -2,10 +2,16 @@
 
 signed int inc_1(signed int i)
 /*@ requires 
-      let MAXi32 = 2147483647i64; 
-      (i64) i + 1i64 <  MAXi32;
-    ensures return == i + 1i32; @*/
+      let MAXi32 = 2147483647; 
+      i + 1 <  MAXi32;
+    ensures return == i + 1; @*/
 {
   i = i + 1;
   return i;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  signed int r = inc_1(24);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/add_5.c b/src/example-archive/simple-examples/working/add_5.c
index e9bc1daf..727f3c2f 100644
--- a/src/example-archive/simple-examples/working/add_5.c
+++ b/src/example-archive/simple-examples/working/add_5.c
@@ -3,11 +3,17 @@
 
 signed int add_5(signed int x, signed int y)
 /*@ requires 
-      let sum = (i64) x + (i64) y;
-      (i64) MINi32() <= sum; sum <= (i64) MAXi32();
+      let sum = x + y;
+      MINi32() <= sum; sum <= MAXi32();
     ensures return == x + y; @*/
 {
   signed int i;
   i = x + y;
   return i;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  signed int r = add_5(100, 102);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/add_uint_1.c b/src/example-archive/simple-examples/working/add_uint_1.c
index 73b0e0e0..d54e9af2 100644
--- a/src/example-archive/simple-examples/working/add_uint_1.c
+++ b/src/example-archive/simple-examples/working/add_uint_1.c
@@ -3,11 +3,17 @@
 
 unsigned int add_uint_1(unsigned int x, unsigned int y)
 /*@ requires 
-      let MAXi32 = 2147483647i64;
-      (i64) x + (i64) y <= MAXi32;
+      let MAXi32 = 2147483647;
+      x + y <= MAXi32;
     ensures return == x + y; @*/
 {
   signed int i;
   i = x + y;
   return i;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  unsigned int r = add_uint_1(5, 42);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/array_1.c b/src/example-archive/simple-examples/working/array_1.c
index 8788c081..2bf94a3e 100644
--- a/src/example-archive/simple-examples/working/array_1.c
+++ b/src/example-archive/simple-examples/working/array_1.c
@@ -2,10 +2,10 @@
 
 void array_1(int *arr, int size, int off)
 /*@ requires 
-      take arrayStart = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; 
-      0i32 <= off; 
+      take arrayStart = each (integer j; 0 <= j && j < size) {RW(arr + j)}; 
+      0 <= off; 
       off < size;
-    ensures take arrayEnd = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; @*/
+    ensures take arrayEnd = each (integer j; 0 <= j && j < size) {RW(arr + j)}; @*/
 {
   int i = off;
   /*@ focus RW<int>, i; @*/  // <-- required to read / write
@@ -13,3 +13,10 @@ void array_1(int *arr, int size, int off)
   i++;
   return;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int arr[5] = {1, 4, 6, 9, 10};
+  array_1(arr, 5, 3);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/array_2.c b/src/example-archive/simple-examples/working/array_2.c
index e4b27c3a..19ef7de9 100644
--- a/src/example-archive/simple-examples/working/array_2.c
+++ b/src/example-archive/simple-examples/working/array_2.c
@@ -2,17 +2,25 @@
 
 int array_2(int *arr, int size, int off)
 /*@ requires 
-      take arrayStart = each (i32 j; 0i32  <= j && j < size) {RW(arr + j)};
-      0i32 <= off; 
+      take arrayStart = each (integer j; 0  <= j && j < size) {RW(arr + j)};
+      0 <= off; 
       off < size; 
-      arrayStart[off] != 0i32;
+      arrayStart[off] != 0;
     ensures  
-      take arrayEnd = each (i32 j; 0i32  <= j && j < size) {RW(arr + j)};
-      arrayEnd[off] == 7i32; 
+      take arrayEnd = each (integer j; 0  <= j && j < size) {RW(arr + j)};
+      arrayEnd[off] == 7; 
       return == arrayStart[off]; @*/
 {
   /*@ focus RW<int>, off; @*/
-  int tmp = arr[off];
+  /*@ instantiate off; @*/
+ int tmp = arr[off];
   arr[off] = 7;
   return tmp; 
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int arr[5] = {1, 4, 6, 9, 10};
+  array_2(arr, 5, 3);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/array_3.c b/src/example-archive/simple-examples/working/array_3.c
index d8ffcf33..79f424e8 100644
--- a/src/example-archive/simple-examples/working/array_3.c
+++ b/src/example-archive/simple-examples/working/array_3.c
@@ -4,20 +4,20 @@
 
 void array_3(int *arr, int n)
 /*@ requires 
-      0i32 < n;
-      take arrayStart = each (i32 j; 0i32 <= j && j < n) {RW<int>(arr + j)};
+      0 < n;
+      take arrayStart = each (integer j; 0 <= j && j < n) {RW<int>(arr + j)};
     ensures 
-      take arrayEnd = each (i32 j; 0i32 <= j && j < n) {RW<int>(arr + j)};
-      each (i32 j; 0i32 <= j && j < n) {arrayEnd[j] == 7i32}; @*/
+      take arrayEnd = each (integer j; 0 <= j && j < n) {RW<int>(arr + j)};
+      each (integer j; 0 <= j && j < n) {arrayEnd[j] == 7}; @*/
 {
   int i = 0;
   while (i < n)
   /*@ inv {n}unchanged; 
           {arr}unchanged;
-          0i32 <= i; 
+          0 <= i; 
           i <= n;
-          take arrayInv = each (i32 j; 0i32 <= j && j < n) {RW<int>(arr + j)};
-          each (i32 j; 0i32 <= j && j < i) {arrayInv[j] == 7i32}; @*/ 
+          take arrayInv = each (integer j; 0 <= j && j < n) {RW<int>(arr + j)};
+          each (integer j; 0 <= j && j < i) {arrayInv[j] == 7}; @*/ 
   {
     /*@ focus RW<int>, i; @*/
     *(arr + i) = 7;
@@ -25,3 +25,10 @@ void array_3(int *arr, int n)
   };
   return;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int arr[5] = {1, 4, 6, 9, 10};
+  array_3(arr, 5);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/array_4.c b/src/example-archive/simple-examples/working/array_4.c
index 81a76ec3..05db110f 100644
--- a/src/example-archive/simple-examples/working/array_4.c
+++ b/src/example-archive/simple-examples/working/array_4.c
@@ -1 +1,7 @@
 void a() { int b[] = {0}; }
+
+int main(void)
+/*@ trusted; @*/
+{
+    a();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/array_5.c b/src/example-archive/simple-examples/working/array_5.c
index 81a76ec3..05db110f 100644
--- a/src/example-archive/simple-examples/working/array_5.c
+++ b/src/example-archive/simple-examples/working/array_5.c
@@ -1 +1,7 @@
 void a() { int b[] = {0}; }
+
+int main(void)
+/*@ trusted; @*/
+{
+    a();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/array_6.c b/src/example-archive/simple-examples/working/array_6.c
index ca8aa790..9214cb9c 100644
--- a/src/example-archive/simple-examples/working/array_6.c
+++ b/src/example-archive/simple-examples/working/array_6.c
@@ -1 +1,8 @@
 int a[] = {{5}};
+
+int main(void)
+/*@ trusted; @*/
+{
+    int x = a[0];
+    /*@ assert (x == 5); @*/
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/array_read.c b/src/example-archive/simple-examples/working/array_read.c
index e53e886c..85fe5361 100644
--- a/src/example-archive/simple-examples/working/array_read.c
+++ b/src/example-archive/simple-examples/working/array_read.c
@@ -2,22 +2,22 @@
 int head(int *arr, unsigned long len)
 /*@
 requires
-    take arr_in = each(u64 i; i < len) {
+    take arr_in = each(integer i; i >= 0 && i < len) {
         RW(array_shift<int>(arr, i))
     };
-    each(u64 i; i < len) {
-        arr_in[i] == 0i32
+    each(integer i; i >= 0 && i < len) {
+        arr_in[i] == 0
     };
-    len > 0u64;
+    len > 0;
 
 ensures
-    take arr_out = each(u64 i; i < len) {
+    take arr_out = each(integer i; i >= 0 && i < len) {
         RW(array_shift<int>(arr, i))
     };
-    each(u64 i; i < len) {
-        arr_out[i] == 0i32
+    each(integer i; i >= 0 && i < len) {
+        arr_out[i] == 0
     };
-    return == 0i32;
+    return == 0;
 @*/
 {
     unsigned long idx = 0;
@@ -26,6 +26,7 @@ ensures
     // iterated resource `arr_in`, which it needs in order to verify the
     // following read:
     /*@ focus RW<int>, idx; @*/
+    /*@ instantiate idx; @*/
 
     int hd = arr[idx];
 
@@ -42,3 +43,10 @@ ensures
     // that we already required that `len > 0u64`.)
     return hd;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int arr[5] = {0, 0, 0, 0, 0};
+  head(arr, 5);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/assert_1.c b/src/example-archive/simple-examples/working/assert_1.c
index dbadae88..d5fcd4fe 100644
--- a/src/example-archive/simple-examples/working/assert_1.c
+++ b/src/example-archive/simple-examples/working/assert_1.c
@@ -3,21 +3,33 @@
 #include <assert.h>
 
 int assert_1(int x)
-/*@ requires x == 7i32;
-    ensures return == 0i32; @*/
+/*@ requires x == 7;
+    ensures return == 0; @*/
 {
   x = 0;
+  #ifdef CN_INSTRUMENT
+  /*@ assert(x == 0); @*/
+  #else
   assert(x == 0);
+  #endif
   return (x);
 }
 
 // An alternative syntax for the same assertion: 
 
 int assert_1_alt(int x)
-/*@ requires x == 7i32;
-    ensures return == 0i32; @*/
+/*@ requires x == 7;
+    ensures return == 0; @*/
 {
   x = 0;
-  /*@ assert(x == 0i32); @*/
+  /*@ assert(x == 0); @*/
   return (x);
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 7;
+  assert_1(x);
+  assert_1_alt(x);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/assert_2.c b/src/example-archive/simple-examples/working/assert_2.c
index 116b6051..ae441ff1 100644
--- a/src/example-archive/simple-examples/working/assert_2.c
+++ b/src/example-archive/simple-examples/working/assert_2.c
@@ -4,14 +4,30 @@ void assert_2(int *x, int *y)
 /*@ requires 
       take Xpre = RW<int>(x); 
       take Ypre = RW<int>(y);
-      *x == 7i32; *y == 7i32;
+      *x == 7; *y == 7;
     ensures 
       take Xpost = RW<int>(x);
       take Ypost = RW<int>(y);
-      *x == 0i32; *y == 0i32; @*/
+      *x == 0; *y == 0; @*/
 {
   *x = 0;
+  #ifdef CN_INSTRUMENT
+  /*@ assert(*x == 0 && *y == 7); @*/
+  #else
   assert(*x == 0 && *y == 7);
+  #endif
   *y = 0;
+  #ifdef CN_INSTRUMENT
+  /*@ assert(*x == 0 && *y == 0); @*/
+  #else
   assert(*x == 0 && *y == 0);
+  #endif
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 7;
+  int y = 7;
+  assert_2(&x, &y);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/assert_3.c b/src/example-archive/simple-examples/working/assert_3.c
index ebd9a385..39ca69c1 100644
--- a/src/example-archive/simple-examples/working/assert_3.c
+++ b/src/example-archive/simple-examples/working/assert_3.c
@@ -14,21 +14,41 @@ void assert_3(int *x, int *y)
 /*@ requires 
       take Xpre = RW<int>(x); 
       take Ypre = RW<int>(y);
-      *x == 7i32; *y == 7i32;
+      *x == 7; *y == 7;
     ensures 
       take Xpost = RW<int>(x);
       take Ypost = RW<int>(y);
-      *x == 0i32; *y == 0i32; @*/
+      *x == 0; *y == 0; @*/
 {
   *x = 0;
+  #ifdef CN_INSTRUMENT
+  /*@ assert(*x == 0 && *y == 7); @*/
+  #else
   assert(*x == 0 && *y == 7);
-
+  #endif
   // Apply the lemma to x / y 
   /*@ apply assert_own(x); @*/
   /*@ apply assert_own(y); @*/
 
+  #ifdef CN_INSTRUMENT
+  /*@ assert(*x == 0 && *y == 7); @*/
+  #else
   assert(*x == 0 && *y == 7);
+  #endif
+  
   *y = 0;
+
+  #ifdef CN_INSTRUMENT
+  /*@ assert(*x == 0 && *y == 0); @*/
+  #else
   assert(*x == 0 && *y == 0);
+  #endif
 }
 
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 7;
+  int y = 7;
+  assert_3(&x, &y);
+}
diff --git a/src/example-archive/simple-examples/working/bit_compl_1.c b/src/example-archive/simple-examples/working/bit_compl_1.c
index 0880e08b..1a34d789 100644
--- a/src/example-archive/simple-examples/working/bit_compl_1.c
+++ b/src/example-archive/simple-examples/working/bit_compl_1.c
@@ -1 +1,7 @@
 void a() { ~0; }
+
+int main(void)
+/*@ trusted; @*/
+{
+  a();
+}
diff --git a/src/example-archive/simple-examples/working/cast_1.c b/src/example-archive/simple-examples/working/cast_1.c
index 25877d83..9ef4b344 100644
--- a/src/example-archive/simple-examples/working/cast_1.c
+++ b/src/example-archive/simple-examples/working/cast_1.c
@@ -5,7 +5,7 @@
 #include <stdint.h> // For uintptr_t, intptr_t
 
 int cast_1()
-/*@ ensures return == 7i32; @*/
+/*@ ensures return == 7; @*/
 {
   int x = 7;
   int *ptr_original = &x;
@@ -21,3 +21,9 @@ int cast_1()
 
   return ret;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  cast_1();
+}
diff --git a/src/example-archive/simple-examples/working/cast_2.c b/src/example-archive/simple-examples/working/cast_2.c
index e2b548f6..4ee11fee 100644
--- a/src/example-archive/simple-examples/working/cast_2.c
+++ b/src/example-archive/simple-examples/working/cast_2.c
@@ -4,7 +4,7 @@
 #include <stdint.h> // For uintptr_t, intptr_t
 
 int cast_2()
-/*@ ensures return == 7i32; @*/
+/*@ ensures return == 7; @*/
 {
   int x = 7;
   int *ptr_original = &x;
@@ -27,3 +27,9 @@ int cast_2()
     return 7; 
   }
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  cast_2();
+}
diff --git a/src/example-archive/simple-examples/working/cast_3.c b/src/example-archive/simple-examples/working/cast_3.c
index 09150429..b8f51d43 100644
--- a/src/example-archive/simple-examples/working/cast_3.c
+++ b/src/example-archive/simple-examples/working/cast_3.c
@@ -5,7 +5,7 @@
 #define OFFSET 374328
 
 int cast_3()
-/*@ ensures return == 7i32; @*/
+/*@ ensures return == 7; @*/
 {
   int x = 7;
   int *ptr_original = &x;
@@ -28,3 +28,9 @@ int cast_3()
     return 7; 
   }
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  cast_3();
+}
diff --git a/src/example-archive/simple-examples/working/cast_4.c b/src/example-archive/simple-examples/working/cast_4.c
index 9667fe97..951df94d 100644
--- a/src/example-archive/simple-examples/working/cast_4.c
+++ b/src/example-archive/simple-examples/working/cast_4.c
@@ -7,7 +7,7 @@
 int cast_4(int *ptr_original)
 /*@ requires take Pre = W<int>(ptr_original);
     ensures take Post = RW<int>(ptr_original);
-            return == 7i32; @*/
+            return == 7; @*/
 {
   *ptr_original = 7;
   // Cast pointer to uintptr_t
@@ -28,3 +28,10 @@ int cast_4(int *ptr_original)
     return 7; 
   }
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 42;
+  cast_4(&x);
+}
diff --git a/src/example-archive/simple-examples/working/cond_1.c b/src/example-archive/simple-examples/working/cond_1.c
index 7947bc1e..564b571e 100644
--- a/src/example-archive/simple-examples/working/cond_1.c
+++ b/src/example-archive/simple-examples/working/cond_1.c
@@ -2,11 +2,17 @@
 
 int cond_1 (int i) 
 /*@ ensures 
-      return == (i == 0i32 ? 0i32 : 1i32); @*/
+      return == (i == 0 ? 0 : 1); @*/
 {
   if (i == 0) {
     return 0; 
   } else {
     return 1; 
   }
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  cond_1(0);
 }
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/dec_1.c b/src/example-archive/simple-examples/working/dec_1.c
index b4a07231..9e918d91 100644
--- a/src/example-archive/simple-examples/working/dec_1.c
+++ b/src/example-archive/simple-examples/working/dec_1.c
@@ -1,23 +1,39 @@
 // Pre and post-read decrement 
 
 int dec_1_pre(int i) 
-/*@ requires i >= 1i32;
-    ensures return == i - 1i32; @*/
+/*@ requires i >= 1;
+    ensures return == i - 1; @*/
 { 
   int start, pre, post; 
   start = i; 
   pre = --i; 
+  #ifdef CN_INSTRUMENT
+  /*@ assert(pre == start-1); @*/
+  #else
   assert(pre == start-1);
+  #endif
   return i; 
 }
 
 int dec_1_post(int i) 
-/*@ requires i >= 1i32;
-    ensures return == i - 1i32; @*/
+/*@ requires i >= 1;
+    ensures return == i - 1; @*/
 { 
   int start, pre, post; 
   start = i; 
   pre = i--; 
+  #ifdef CN_INSTRUMENT
+  /*@ assert(pre == start); @*/
+  #else
   assert(pre == start);
-  return i; 
+  #endif
+  return i;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int i = 42;
+  dec_1_pre(i);
+  dec_1_post(i);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/division.c b/src/example-archive/simple-examples/working/division.c
index 62d286b9..e8e0b9d2 100644
--- a/src/example-archive/simple-examples/working/division.c
+++ b/src/example-archive/simple-examples/working/division.c
@@ -1 +1,7 @@
 void a() { 1 / 1; }
+
+int main(void)
+/*@ trusted; @*/
+{
+    a();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/effect_1.c b/src/example-archive/simple-examples/working/effect_1.c
index 70012209..89a3aa4e 100644
--- a/src/example-archive/simple-examples/working/effect_1.c
+++ b/src/example-archive/simple-examples/working/effect_1.c
@@ -10,7 +10,7 @@ write_g_to_1()
         take Pre = W<int>(&g);
     ensures 
         take Post = RW<int>(&g); 
-        Post == 1i32; @*/
+        Post == 1; @*/
 {
 	g = 1;
 }
@@ -22,7 +22,7 @@ effect_1()
       take Pre = W<int>(&g);
     ensures 
       take Post = RW<int>(&g); 
-      return == 1i32; @*/
+      return == 1; @*/
 {
   int x;
   
@@ -32,3 +32,9 @@ effect_1()
     return 1;
   return 0; 
 } 
+
+int main(void)
+/*@ trusted; @*/
+{
+    int r = effect_1();
+}
diff --git a/src/example-archive/simple-examples/working/for_1.c b/src/example-archive/simple-examples/working/for_1.c
index 244f4a31..3c1416fd 100644
--- a/src/example-archive/simple-examples/working/for_1.c
+++ b/src/example-archive/simple-examples/working/for_1.c
@@ -9,3 +9,9 @@ int for_1()
   }; 
   return acc;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int r = for_1();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/for_2.c b/src/example-archive/simple-examples/working/for_2.c
index 67a4a5e9..07b582f7 100644
--- a/src/example-archive/simple-examples/working/for_2.c
+++ b/src/example-archive/simple-examples/working/for_2.c
@@ -5,11 +5,17 @@ int for_2()
   int acc = 0; 
   int i; 
   for(i = 0; i < 10; i++)
-  /*@ inv 0i32 <= i; 
-          i <= 10i32;
-          acc <= 10i32; @*/
+  /*@ inv 0 <= i; 
+          i <= 10;
+          acc <= 10; @*/
   {
     acc = i; 
   }; 
   return acc;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int r = for_2();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/for_3.c b/src/example-archive/simple-examples/working/for_3.c
index e8e895c0..3e5a7ea9 100644
--- a/src/example-archive/simple-examples/working/for_3.c
+++ b/src/example-archive/simple-examples/working/for_3.c
@@ -1,15 +1,22 @@
 // A trivial for-loop 
 // TODO: doesn't parse 
+// TODO: Fix for-loops in Fulminate
 
 int for_3() 
 {
   int acc = 0; 
   for(int i = 0; i < 10; i++) 
-  /*@ inv 0i32 <= i; 
-          i <= 10i32;
-          acc <= 10i32; @*/
+  /*@ inv 0 <= i; 
+          i <= 10;
+          acc <= 10; @*/
   {
     acc = i; 
   }; 
   return acc;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int r = for_3();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/free_1.c b/src/example-archive/simple-examples/working/free_1.c
index 94f14b9a..53171c71 100644
--- a/src/example-archive/simple-examples/working/free_1.c
+++ b/src/example-archive/simple-examples/working/free_1.c
@@ -3,10 +3,18 @@
 // free() is not defined by default in CN. We can define a fake version that
 // only works on ints.
 
+#ifdef CN_INSTRUMENT
+void cn_free_sized(void*, unsigned long len);
+#endif
+
 void my_free_int(int *target)
 /*@ trusted;
     requires take ToFree = RW<int>(target); @*/
-{}
+{
+  #ifdef CN_INSTRUMENT
+  cn_free_sized(target, sizeof(int));
+  #endif
+}
 
 void free_1(int *x, int *y)
 /*@ requires 
@@ -18,3 +26,13 @@ void free_1(int *x, int *y)
   my_free_int(x);
   // *x = 7; // <-- Would generate an error
 }
+
+
+int main(void)
+/*@ trusted; @*/
+{
+  #ifdef CN_INSTRUMENT
+  int x = 5, y = 42;
+  free_1(&x, &y);
+  #endif
+}
diff --git a/src/example-archive/simple-examples/working/inc_1.c b/src/example-archive/simple-examples/working/inc_1.c
index 2d52e8ed..9d731e53 100644
--- a/src/example-archive/simple-examples/working/inc_1.c
+++ b/src/example-archive/simple-examples/working/inc_1.c
@@ -1,26 +1,42 @@
 
 int inc_1_pre(int i) 
 /*@ requires 
-      let MAXi32 = 2147483647i64; 
-      (i64) i + 1i64 <  MAXi32;
-    ensures return == i + 1i32; @*/
+      let MAXi32 = 2147483647; 
+      i + 1 <  MAXi32;
+    ensures return == i + 1; @*/
 { 
   int start, pre, post; 
   start = i; 
   pre = ++i; 
+  #ifdef CN_INSTRUMENT
+  /*@ assert(pre == start+1); @*/
+  #else
   assert(pre == start+1);
+  #endif
   return i; 
 }
 
 int inc_1_post(int i) 
 /*@ requires 
-      let MAXi32 = 2147483647i64; 
-      (i64) i + 1i64 <  MAXi32;
-    ensures return == i + 1i32; @*/
+      let MAXi32 = 2147483647; 
+      i + 1 <  MAXi32;
+    ensures return == i + 1; @*/
 { 
   int start, pre, post; 
   start = i; 
   pre = i++; 
+  #ifdef CN_INSTRUMENT
+  /*@ assert(pre == start); @*/
+  #else
   assert(pre == start);
+  #endif
   return i; 
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int i = 42;
+  inc_1_pre(i);
+  inc_1_post(i);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/int_to_char_1.c b/src/example-archive/simple-examples/working/int_to_char_1.c
index bbe6d9d1..aaeb3115 100644
--- a/src/example-archive/simple-examples/working/int_to_char_1.c
+++ b/src/example-archive/simple-examples/working/int_to_char_1.c
@@ -5,10 +5,17 @@
 void 
 int_to_char_1(int a) 
 /*@ requires 
-      (i32) MINu8() <= (i32) a; 
-      (i32) a <= (i32) MAXu8(); @*/
+      MINu8() <= a; 
+      a <= MAXu8(); @*/
 {
   char b; 
   b = a; 
   return; 
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  int i = 42;
+  int_to_char_1(i);
 }
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/lemma_1.c b/src/example-archive/simple-examples/working/lemma_1.c
index bc701fee..60c54825 100644
--- a/src/example-archive/simple-examples/working/lemma_1.c
+++ b/src/example-archive/simple-examples/working/lemma_1.c
@@ -10,4 +10,10 @@ void lemma_1()
 {
   /*@ apply lem_trivial(); @*/
   ; 
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  lemma_1();
 }
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/list_1.c b/src/example-archive/simple-examples/working/list_1.c
index 7ef17d6b..1c165392 100644
--- a/src/example-archive/simple-examples/working/list_1.c
+++ b/src/example-archive/simple-examples/working/list_1.c
@@ -13,3 +13,21 @@ struct list_node *list_1(struct list_node *xs)
   ys = xs;
   return ys;
 }
+
+void *cn_malloc(unsigned long size);
+
+int main(void)
+/*@ trusted; @*/
+{
+  // Constructs list with values [2, 4, 6]
+  struct list_node *n3 = cn_malloc(sizeof(struct list_node));
+  n3->val = 6;
+  n3->next = 0;
+  struct list_node *n2 = cn_malloc(sizeof(struct list_node));
+  n2->val = 4;
+  n2->next = n3;
+  struct list_node *n1 = cn_malloc(sizeof(struct list_node));
+  n1->val = 2;
+  n1->next = n2;
+  list_1(n1);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/list_2.c b/src/example-archive/simple-examples/working/list_2.c
index 8d8b003c..0d5ab4ae 100644
--- a/src/example-archive/simple-examples/working/list_2.c
+++ b/src/example-archive/simple-examples/working/list_2.c
@@ -37,3 +37,20 @@ void list_2(struct list_node *head)
   return;
 }
 
+void *cn_malloc(unsigned long size);
+
+int main(void)
+/*@ trusted; @*/
+{
+  // Constructs list with values [2, 4, 6]
+  struct list_node *n3 = cn_malloc(sizeof(struct list_node));
+  n3->val = 6;
+  n3->next = 0;
+  struct list_node *n2 = cn_malloc(sizeof(struct list_node));
+  n2->val = 4;
+  n2->next = n3;
+  struct list_node *n1 = cn_malloc(sizeof(struct list_node));
+  n1->val = 2;
+  n1->next = n2;
+  list_2(n1);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/list_3.c b/src/example-archive/simple-examples/working/list_3.c
index f6caead3..84ba8acc 100644
--- a/src/example-archive/simple-examples/working/list_3.c
+++ b/src/example-archive/simple-examples/working/list_3.c
@@ -3,11 +3,11 @@
 
 #include "list_preds.h"
 
-// This version of the predicate takes an i32 argument. Every node in the list
+// This version of the predicate takes an integer argument. Every node in the list
 // must store this value. 
 
 /*@
-predicate [rec] (datatype seq) IntListSegVal(pointer p, pointer tail, i32 tval) {
+predicate [rec] (datatype seq) IntListSegVal(pointer p, pointer tail, integer tval) {
   if (addr_eq(p,tail)) {
     return Seq_Nil{};
   } else {
@@ -20,7 +20,7 @@ predicate [rec] (datatype seq) IntListSegVal(pointer p, pointer tail, i32 tval)
 }
 @*/
 /*@
-lemma IntListSeqSnocVal(pointer p, pointer tail, i32 tval)
+lemma IntListSeqSnocVal(pointer p, pointer tail, integer tval)
   requires take l1 = IntListSegVal(p, tail, tval);
            take v = RW<struct list_node>(tail);
            v.val == tval; 
@@ -31,13 +31,13 @@ lemma IntListSeqSnocVal(pointer p, pointer tail, i32 tval)
 
 void list_3(struct list_node *head)
 /*@ requires take Xs = IntListSeg(head,NULL);
-    ensures  take Ys = IntListSegVal(head,NULL,7i32); @*/
+    ensures  take Ys = IntListSegVal(head,NULL,7); @*/
 {
   struct list_node *curr;
   curr = head;
 
   while (curr != 0)
-  /*@ inv take Visited = IntListSegVal(head,curr,7i32);
+  /*@ inv take Visited = IntListSegVal(head,curr,7);
           take Remaining = IntListSeg(curr,NULL);
           {head}unchanged;
           let i_curr = curr; 
@@ -45,7 +45,25 @@ void list_3(struct list_node *head)
   {
     curr->val = 7;
     curr = curr->next;
-    /*@ apply IntListSeqSnocVal(head, i_curr, 7i32); @*/
+    /*@ apply IntListSeqSnocVal(head, i_curr, 7); @*/
   }
   return;
 }
+
+void *cn_malloc(unsigned long size);
+
+int main(void)
+/*@ trusted; @*/
+{
+  // Constructs list with values [2, 4, 6]
+  struct list_node *n3 = cn_malloc(sizeof(struct list_node));
+  n3->val = 6;
+  n3->next = 0;
+  struct list_node *n2 = cn_malloc(sizeof(struct list_node));
+  n2->val = 4;
+  n2->next = n3;
+  struct list_node *n1 = cn_malloc(sizeof(struct list_node));
+  n1->val = 2;
+  n1->next = n2;
+  list_3(n1);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/list_4.c b/src/example-archive/simple-examples/working/list_4.c
index 3fadf76c..90c4e92b 100644
--- a/src/example-archive/simple-examples/working/list_4.c
+++ b/src/example-archive/simple-examples/working/list_4.c
@@ -26,3 +26,21 @@ struct list_node *list_reverse_1(struct list_node *head)
   return prev;
 }
 
+
+void *cn_malloc(unsigned long size);
+
+int main(void)
+/*@ trusted; @*/
+{
+  // Constructs list with values [2, 4, 6]
+  struct list_node *n3 = cn_malloc(sizeof(struct list_node));
+  n3->val = 6;
+  n3->next = 0;
+  struct list_node *n2 = cn_malloc(sizeof(struct list_node));
+  n2->val = 4;
+  n2->next = n3;
+  struct list_node *n1 = cn_malloc(sizeof(struct list_node));
+  n1->val = 2;
+  n1->next = n2;
+  list_reverse_1(n1);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/list_preds.h b/src/example-archive/simple-examples/working/list_preds.h
index 7b0b4c2e..c929faf7 100644
--- a/src/example-archive/simple-examples/working/list_preds.h
+++ b/src/example-archive/simple-examples/working/list_preds.h
@@ -15,7 +15,7 @@ struct list_node
 /*@
 datatype seq {
   Seq_Nil {},
-  Seq_Cons { i32 val, datatype seq next}
+  Seq_Cons { integer val, datatype seq next}
 }
 @*/
 
@@ -51,7 +51,7 @@ function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
 @*/
 
 // /*@
-// function [rec] (boolean) fold_eq(datatype seq xs, i32 test) {
+// function [rec] (boolean) fold_eq(datatype seq xs, integer test) {
 //   match xs {
 //     Seq_Nil {} => {
 //       true 
diff --git a/src/example-archive/simple-examples/working/long_type.c b/src/example-archive/simple-examples/working/long_type.c
index abf9b50b..2659547f 100644
--- a/src/example-archive/simple-examples/working/long_type.c
+++ b/src/example-archive/simple-examples/working/long_type.c
@@ -5,4 +5,10 @@
 void long_type_err_1() { 
   -1l; 
   return; 
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  long_type_err_1();
 }
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/loop_1.c b/src/example-archive/simple-examples/working/loop_1.c
index a68e8712..4d17a69a 100644
--- a/src/example-archive/simple-examples/working/loop_1.c
+++ b/src/example-archive/simple-examples/working/loop_1.c
@@ -2,9 +2,9 @@
 // assignment never happens. 
 
 int loop_1()
-/*@ ensures return == 7i32; @*/
+/*@ ensures return == 7; @*/
 {
-  int i = 0;
+  int i = 7;
   while (i != 7)
   {
     i = 42; // Unreachable 
@@ -12,3 +12,8 @@ int loop_1()
   return i;
 }
 
+int main(void)
+/*@ trusted; @*/
+{
+  loop_1();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/loop_2.c b/src/example-archive/simple-examples/working/loop_2.c
index 2b305927..96cc7339 100644
--- a/src/example-archive/simple-examples/working/loop_2.c
+++ b/src/example-archive/simple-examples/working/loop_2.c
@@ -3,13 +3,19 @@
 // including false
 
 int loop_2()
-/*@ ensures return == 42i32; @*/  // <-- Oops, prove whatever we want 
+/*@ ensures return == 42; @*/  // <-- Oops, prove whatever we want 
 {
   int i = 0;
   while (i < 10)
-  /*@ inv i == 0i32; @*/  // <-- Loop exit condition never satisfied
+  /*@ inv i == 0; @*/  // <-- Loop exit condition never satisfied
   {
     // Don't do anything
   };
   return 7; 
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  loop_2();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/loop_3.c b/src/example-archive/simple-examples/working/loop_3.c
index fc60916b..8c768b90 100644
--- a/src/example-archive/simple-examples/working/loop_3.c
+++ b/src/example-archive/simple-examples/working/loop_3.c
@@ -5,9 +5,9 @@
 
 int loop_3(int i)
 /*@ requires 
-      let MAXi32 = (i64) 2147483647i64; // TODO: lift to library 
-      (i64) i + 1i64 <  MAXi32; 
-      0i32 < i; @*/
+      let MAXi32 = 2147483647; // TODO: lift to library 
+      i + 1 <  MAXi32; 
+      0 < i; @*/
 // TODO: ensures? 
 {
   int n = 0;
@@ -15,7 +15,7 @@ int loop_3(int i)
 
   while (n != i)
   /*@ inv n <= i; 
-          0i32 <= acc; 
+          0 <= acc; 
           acc <= n; @*/
   {
     acc = n - acc;
@@ -23,3 +23,9 @@ int loop_3(int i)
   };
   return acc;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  loop_3(42);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/loop_4.c b/src/example-archive/simple-examples/working/loop_4.c
index 1c10cb40..752119e2 100644
--- a/src/example-archive/simple-examples/working/loop_4.c
+++ b/src/example-archive/simple-examples/working/loop_4.c
@@ -2,15 +2,15 @@
 // although actually we could definitely bounded-model-check it
 
 int loop_4()
-/*@ ensures return == 1i32; @*/
+/*@ ensures return == 1; @*/
 {
   int n = 0;
   int acc = 0;
 
   while (n < 1)
-  /*@ inv (n == 0i32 && acc == 0i32)
+  /*@ inv (n == 0 && acc == 0)
           ||
-          (n == 1i32 && acc == 1i32); @*/
+          (n == 1 && acc == 1); @*/
   {
     n++;
     acc++;
@@ -18,3 +18,8 @@ int loop_4()
   return acc;
 }
 
+int main(void)
+/*@ trusted; @*/
+{
+  loop_4();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/loop_5.c b/src/example-archive/simple-examples/working/loop_5.c
index ef30322e..fe2a2786 100644
--- a/src/example-archive/simple-examples/working/loop_5.c
+++ b/src/example-archive/simple-examples/working/loop_5.c
@@ -1,16 +1,22 @@
 // A loop with a simple post-condition
 
 int loop_5()
-/*@ ensures return == 7i32; @*/
+/*@ ensures return == 7; @*/
 {
   int ret = 0;
   int i = 0;
   while (i < 7)
   /*@ inv ret == i;
-          i <= 7i32; @*/
+          i <= 7; @*/
   {
     i = i + 1;
     ret = i;
   }; // The exit condition implies the post-condition 
   return ret;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  loop_5();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/loop_6.c b/src/example-archive/simple-examples/working/loop_6.c
index 5113a5f2..aadddee3 100644
--- a/src/example-archive/simple-examples/working/loop_6.c
+++ b/src/example-archive/simple-examples/working/loop_6.c
@@ -1,14 +1,20 @@
 // A loop with a post-condition and a very big arbitrary constant
 
 int loop_6(int n)
-/*@ ensures return == 789398323i32; @*/ // <-- arbitrary value 
+/*@ ensures return == 789398323; @*/ // <-- arbitrary value 
 {
   int i = 0;
   while (i < 789398323)
-  /*@ inv 0i32 <= i; 
-          i <= 789398323i32; @*/
+  /*@ inv 0 <= i; 
+          i <= 789398323; @*/
   {
     i = i + 1;
   };
   return i;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  loop_6(410);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/loop_7.c b/src/example-archive/simple-examples/working/loop_7.c
index 5cc40f7a..47be9200 100644
--- a/src/example-archive/simple-examples/working/loop_7.c
+++ b/src/example-archive/simple-examples/working/loop_7.c
@@ -3,12 +3,12 @@
 // that the value of `n` is unknown, which causes the proof to fail 
 
 int loop_7(int n)
-/*@ requires 0i32 < n;
+/*@ requires 0 < n;
     ensures return == n; @*/
 {
   int i = 0;
   while (i < n)
-  /*@ inv 0i32 <= i; 
+  /*@ inv 0 <= i; 
           i <= n;
           {n}unchanged; @*/ 
   {
@@ -16,3 +16,9 @@ int loop_7(int n)
   };
   return i;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  loop_7(500);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/loop_8.c b/src/example-archive/simple-examples/working/loop_8.c
index f65fbed0..d0a41750 100644
--- a/src/example-archive/simple-examples/working/loop_8.c
+++ b/src/example-archive/simple-examples/working/loop_8.c
@@ -1,15 +1,21 @@
 // A loop with an interesting arithmetic bound  
 
 int loop_8()
-/*@ ensures return > 0i32; @*/
+/*@ ensures return > 0; @*/
 {
   int j=0;
   for (int i=0; i<10; i++)
-  /*@ inv 0i32 <= j; j <= i * 10i32;
-          0i32 <= i; i <= 10i32;
-          (i - 1i32) <= j; @*/
+  /*@ inv 0 <= j; j <= i * 10;
+          0 <= i; i <= 10;
+          (i - 1) <= j; @*/
   {
     j+=i;
   }
   return j;
 } 
+
+int main(void)
+/*@ trusted; @*/
+{
+  loop_8();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/malloc_1.c b/src/example-archive/simple-examples/working/malloc_1.c
index 77c45068..332abe3a 100644
--- a/src/example-archive/simple-examples/working/malloc_1.c
+++ b/src/example-archive/simple-examples/working/malloc_1.c
@@ -3,19 +3,35 @@
 // malloc() is not defined by default in CN. We can define a fake malloc()
 // function that only works on ints.
 
+#ifdef CN_INSTRUMENT
+void* cn_malloc(unsigned long size);
+#endif 
+
 int *my_malloc__int()
 /*@ trusted;
     ensures take New = W<int>(return); @*/
-{}
+{
+  #ifdef CN_INSTRUMENT
+  int *p = cn_malloc(sizeof(int));
+  return p;
+  #endif
+}
 
 int *malloc__1()
 /*@ ensures 
       take New = RW<int>(return);
-      New == 7i32;
-      *return == 7i32; @*/  // <-- Alternative syntax 
+      New == 7;
+      *return == 7; @*/  // <-- Alternative syntax 
 {
   int *new;
   new = my_malloc__int();
   *new = 7; // Have to initialize the memory before it's RW
   return new;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  my_malloc__int();
+}
+
diff --git a/src/example-archive/simple-examples/working/mult_timeout.c b/src/example-archive/simple-examples/working/mult_timeout.c
new file mode 100644
index 00000000..87c7c02d
--- /dev/null
+++ b/src/example-archive/simple-examples/working/mult_timeout.c
@@ -0,0 +1,31 @@
+// Filed by @lwli11, see https://github.com/rems-project/cerberus/issues/856
+
+#include <limits.h>
+
+/*@  
+lemma div(integer x, integer y)
+  requires let b1 = 0 <= x && x <= MAXi32();
+           let b2 = 0 <= y && y <= MAXi32();
+  ensures (b1 && b2) implies (0 <= x / y && x / y <= MAXi32());
+
+lemma mul_div(integer a, integer b, integer n)
+  requires a > 0; b > 0; n > 0;
+           a < n / b;
+  ensures  0 < a*b; a*b < n;
+@*/
+
+int mult_timeout(int a, int b){
+  /*@ apply div(MAXi32(),b); @*/
+  if (a > 0 && b>0 && INT_MAX / b > a){
+    /*@ apply mul_div(a,b,MAXi32()); @*/
+    return a*b;
+  }
+  return 0;
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  int r = mult_timeout(5, 42);
+  /*@ assert (r == 210); @*/
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/neg_1.c b/src/example-archive/simple-examples/working/neg_1.c
index 0f1d456c..6fd06d73 100644
--- a/src/example-archive/simple-examples/working/neg_1.c
+++ b/src/example-archive/simple-examples/working/neg_1.c
@@ -1,5 +1,12 @@
 int neg_1(int i) 
-/*@ requires -i > MINi32(); @*/
+/*@ requires i > MINi32(); @*/
 {
   return -i; 
+}
+
+int main(void)
+/*@ trusted; @*/
+{
+  int r = neg_1(42);
+  /*@ assert (r == -42); @*/
 }
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/pointer_dec1.c b/src/example-archive/simple-examples/working/pointer_dec1.c
index 33e87bae..96a5cf1d 100644
--- a/src/example-archive/simple-examples/working/pointer_dec1.c
+++ b/src/example-archive/simple-examples/working/pointer_dec1.c
@@ -3,3 +3,9 @@ void b() {
   int *c = &a[1];
   c -= 1;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  b();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/pointer_dec2.c b/src/example-archive/simple-examples/working/pointer_dec2.c
index 058880fc..e2edeb18 100644
--- a/src/example-archive/simple-examples/working/pointer_dec2.c
+++ b/src/example-archive/simple-examples/working/pointer_dec2.c
@@ -5,3 +5,9 @@ void b() {
   int *c = &a[1];
   --c;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  b();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/power_1.c b/src/example-archive/simple-examples/working/power_1.c
index e76feba5..cc5a8ee7 100644
--- a/src/example-archive/simple-examples/working/power_1.c
+++ b/src/example-archive/simple-examples/working/power_1.c
@@ -7,18 +7,18 @@
 //   1. the base case - power_uf(2,0) = 1 
 //   2. the inductive case - power(2,y+1) == 2 * power_uf(2,y)
 
-/*@ function (i32) power_uf(i32 x, i32 y) @*/
+/*@ function (integer) power_uf(integer x, integer y) @*/
 
 void lemma_power_uf_def(int y)
 /*@ trusted;
-    requires y >= 0i32;
+    requires y >= 0;
     ensures 
-      (power_uf(2i32,0i32)) == 1i32; 
-      (power_uf(2i32,y+1i32)) == (2i32 * power_uf(2i32,y)); @*/
+      (power_uf(2,0)) == 1; 
+      (power_uf(2,y+1)) == (2 * power_uf(2,y)); @*/
 {}
 
 int power_1()
-/*@ ensures return == power_uf(2i32,0i32); @*/
+/*@ ensures return == power_uf(2,0); @*/
 {
   int i = 0;
   int pow = 1;
@@ -29,19 +29,26 @@ int power_1()
 // Variant 2 - define the lemma at the specification level 
 
 /*@
-lemma LemmaPowerUFDef(i32 y)
+lemma LemmaPowerUFDef(integer y)
   requires 
-    y >= 0i32;
+    y >= 0;
   ensures 
-    (power_uf(2i32,0i32)) == 1i32; 
-    (power_uf(2i32,y+1i32)) == (2i32 * power_uf(2i32,y));
+    (power_uf(2,0)) == 1; 
+    (power_uf(2,y+1)) == (2 * power_uf(2,y));
 @*/
 
 int power_1_alt()
-/*@ ensures return == power_uf(2i32,0i32); @*/
+/*@ ensures return == power_uf(2,0); @*/
 {
   int i = 0;
   int pow = 1;
   /*@ apply LemmaPowerUFDef(i); @*/
   return pow;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  power_1();
+  power_1_alt();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/power_2.c b/src/example-archive/simple-examples/working/power_2.c
index 3d7d3444..5bc006ab 100644
--- a/src/example-archive/simple-examples/working/power_2.c
+++ b/src/example-archive/simple-examples/working/power_2.c
@@ -1,19 +1,19 @@
 // Compute 2^1
 
-/*@ function (i32) power_uf(i32 x, i32 y) @*/
+/*@ function (integer) power_uf(integer x, integer y) @*/
 
 
 /*@
-lemma LemmaPowerUFDef(i32 y)
+lemma LemmaPowerUFDef(integer y)
   requires 
-    y >= 0i32; 
+    y >= 0; 
   ensures 
-    (power_uf(2i32,0i32)) == 1i32; 
-    (power_uf(2i32,y+1i32)) == (2i32 * power_uf(2i32,y)); 
+    (power_uf(2,0)) == 1; 
+    (power_uf(2,y+1)) == (2 * power_uf(2,y)); 
 @*/
 
 int power_2()
-/*@ ensures return == power_uf(2i32,1i32); @*/
+/*@ ensures return == power_uf(2,1); @*/
 {
   int i = 0;
   int pow = 1;
@@ -22,3 +22,9 @@ int power_2()
   i = i + 1;
   return pow;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  power_2();
+}
diff --git a/src/example-archive/simple-examples/working/pred_2.c b/src/example-archive/simple-examples/working/pred_2.c
index 211cb49a..e3b35f33 100644
--- a/src/example-archive/simple-examples/working/pred_2.c
+++ b/src/example-archive/simple-examples/working/pred_2.c
@@ -3,17 +3,17 @@
 
 // Variant 1 - this works: 
 /*@ 
-predicate (i32) TestMemoryEqZero_2_var1(pointer p) {
+predicate (integer) TestMemoryEqZero_2_var1(pointer p) {
   take PVal = RW<int>(p); 
   let rval = test_if_zero(PVal); 
   return rval; 
 }
 
-function (i32) test_if_zero(i32 x) {
-  if (x == 0i32) {
-    1i32
+function (integer) test_if_zero(integer x) {
+  if (x == 0) {
+    1
   } else { 
-    0i32 
+    0 
   }
 }
 @*/
@@ -21,26 +21,26 @@ function (i32) test_if_zero(i32 x) {
 void pred_2_var1(int *p) 
 /*@ requires 
       take PreP = RW<int>(p); 
-      PreP == 0i32;
+      PreP == 0;
     ensures 
       take TestP = TestMemoryEqZero_2_var1(p); 
-      TestP == 1i32; @*/
+      TestP == 1; @*/
 { 
   ; 
 }
 
 // Variant 2 - this works: 
 /*@ 
-predicate (i32) TestMemoryEqZero_2_Helper(pointer p, i32 x) {
-  if (x == 0i32) {
-    return 1i32; 
+predicate (integer) TestMemoryEqZero_2_Helper(pointer p, integer x) {
+  if (x == 0) {
+    return 1; 
   } else { 
-    return 0i32; 
+    return 0; 
   }
 }
 
 
-predicate (i32) TestMemoryEqZero_2_var2(pointer p) {
+predicate (integer) TestMemoryEqZero_2_var2(pointer p) {
   take PVal = RW<int>(p); 
   take rval = TestMemoryEqZero_2_Helper(p, PVal); 
   return rval; 
@@ -50,19 +50,19 @@ predicate (i32) TestMemoryEqZero_2_var2(pointer p) {
 void pred_2_var2(int *p) 
 /*@ requires 
       take PreP = RW<int>(p); 
-      PreP == 0i32;
+      PreP == 0;
     ensures 
       take TestP = TestMemoryEqZero_2_var2(p); 
-      TestP == 1i32; @*/
+      TestP == 1; @*/
 { 
   ; 
 }
 
 // Variant 3 - this works: 
 /*@ 
-predicate (i32) TestMemoryEqZero_2_var3(pointer p) {
+predicate (integer) TestMemoryEqZero_2_var3(pointer p) {
   take PVal = RW<int>(p); 
-  let rval = (PVal == 0i32 ? 1i32 : 0i32); 
+  let rval = (PVal == 0 ? 1 : 0); 
   return rval; 
 }
 @*/
@@ -70,11 +70,19 @@ predicate (i32) TestMemoryEqZero_2_var3(pointer p) {
 void pred_2_var3(int *p) 
 /*@ requires 
       take PreP = RW<int>(p); 
-      PreP == 0i32;
+      PreP == 0;
     ensures 
       take TestP = TestMemoryEqZero_2_var3(p); 
-      TestP == 1i32; @*/
+      TestP == 1; @*/
 { 
   ; 
 }
 
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 0;
+  pred_2_var1(&x);
+  pred_2_var2(&x);
+  pred_2_var3(&x);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/ret_1.c b/src/example-archive/simple-examples/working/ret_1.c
index e4a688fa..a66f3729 100644
--- a/src/example-archive/simple-examples/working/ret_1.c
+++ b/src/example-archive/simple-examples/working/ret_1.c
@@ -4,3 +4,9 @@ int ret_1()
 {
   return 0;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  ret_1();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/broken/error-proof/sizeof_1.c b/src/example-archive/simple-examples/working/sizeof_1.c
similarity index 99%
rename from src/example-archive/simple-examples/broken/error-proof/sizeof_1.c
rename to src/example-archive/simple-examples/working/sizeof_1.c
index 06d1ce9d..5865ef68 100644
--- a/src/example-archive/simple-examples/broken/error-proof/sizeof_1.c
+++ b/src/example-archive/simple-examples/working/sizeof_1.c
@@ -8,4 +8,4 @@ main()
 	int size1 = sizeof(int);     // <- works 
 	size1 = size1 + 1; 					 // <- also works 
 	int size2 = sizeof(int) + 1; // <- fails 
-}
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/string_1.c b/src/example-archive/simple-examples/working/string_1.c
index a9c4f72e..cd8fe8c0 100644
--- a/src/example-archive/simple-examples/working/string_1.c
+++ b/src/example-archive/simple-examples/working/string_1.c
@@ -1 +1,7 @@
 void a() { ""; }
+
+int main(void)
+/*@ trusted; @*/
+{
+  a();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/struct_1.c b/src/example-archive/simple-examples/working/struct_1.c
index b16e4e2d..6596e960 100644
--- a/src/example-archive/simple-examples/working/struct_1.c
+++ b/src/example-archive/simple-examples/working/struct_1.c
@@ -11,8 +11,17 @@ void struct_1(struct s *p)
     ensures  
       take StructPost = RW<struct s>(p);
       StructPre.x == StructPost.x;
-      StructPost.y == 0i32; @*/
+      StructPost.y == 0; @*/
 {
   p->y = 0;
   // p->x = 7;  // <-- This would fail
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  struct s s;
+  s.x = 5;
+  s.y = 15;
+  struct_1(&s);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/struct_2.c b/src/example-archive/simple-examples/working/struct_2.c
index 3bce9037..b49f78db 100644
--- a/src/example-archive/simple-examples/working/struct_2.c
+++ b/src/example-archive/simple-examples/working/struct_2.c
@@ -9,7 +9,7 @@ struct s
 };
 
 int struct_2()
-/*@ ensures return == 7i32; @*/
+/*@ ensures return == 7; @*/
 {
   struct s target;
 
@@ -24,6 +24,16 @@ int struct_2()
 
   // Read from field y via pointer arithmetic 
   int ret = *fieldPtr;
-  assert(target.x == 8); 
+  #ifdef CN_INSTRUMENT
+  /*@ assert(target.x == 8); @*/
+  #else
+  assert(target.x == 8);
+  #endif
   return ret;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  struct_2();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/struct_3.c b/src/example-archive/simple-examples/working/struct_3.c
index 9d0b8201..73565b7b 100644
--- a/src/example-archive/simple-examples/working/struct_3.c
+++ b/src/example-archive/simple-examples/working/struct_3.c
@@ -1,3 +1,9 @@
 struct {
   int a;
 } b = {{5}};
+
+int main(void)
+/*@ trusted; @*/
+{
+  /*@ assert (b.a == 5); @*/
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/swap_1.c b/src/example-archive/simple-examples/working/swap_1.c
index 5c2607eb..93a734fe 100644
--- a/src/example-archive/simple-examples/working/swap_1.c
+++ b/src/example-archive/simple-examples/working/swap_1.c
@@ -15,3 +15,10 @@ void swap_1(int *a, int *b)
   // *a = 0;  // <-- This would fail
   *b = temp;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 42, y = 7;
+  swap_1(&x, &y);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/switch_1.c b/src/example-archive/simple-examples/working/switch_1.c
index aabf196e..6b4228ad 100644
--- a/src/example-archive/simple-examples/working/switch_1.c
+++ b/src/example-archive/simple-examples/working/switch_1.c
@@ -2,3 +2,9 @@ void a() {
   switch (0)
     ;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  a();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/voidfn_1.c b/src/example-archive/simple-examples/working/voidfn_1.c
index ee159222..1d178bca 100644
--- a/src/example-archive/simple-examples/working/voidfn_1.c
+++ b/src/example-archive/simple-examples/working/voidfn_1.c
@@ -1 +1,7 @@
 void a() { return; }
+
+int main(void)
+/*@ trusted; @*/
+{
+  a();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/write_1.c b/src/example-archive/simple-examples/working/write_1.c
index 0024b2b7..276f9185 100644
--- a/src/example-archive/simple-examples/working/write_1.c
+++ b/src/example-archive/simple-examples/working/write_1.c
@@ -4,7 +4,14 @@ void write_1(int *cell)
 /*@ requires take CellPre = RW<int>(cell);
     ensures 
       take CellPost = RW<int>(cell);
-      CellPost == 7i32; @*/
+      CellPost == 7; @*/
 {
   *cell = 7;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x = 10;
+  write_1(&x);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/write_2.c b/src/example-archive/simple-examples/working/write_2.c
index c4b25573..da02ccee 100644
--- a/src/example-archive/simple-examples/working/write_2.c
+++ b/src/example-archive/simple-examples/working/write_2.c
@@ -5,8 +5,15 @@ void write_2(int *cell1, int *cell2)
              take Cell2Pre = RW<int>(cell2);
     ensures take Cell1Post = RW<int>(cell1);
             take Cell2Post = RW<int>(cell2);
-            Cell1Post == 7i32; Cell2Post == 8i32; @*/
+            Cell1Post == 7; Cell2Post == 8; @*/
 {
   *cell1 = 7;
   *cell2 = 8;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x, y;
+  write_2(&x, &y);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/write_3.c b/src/example-archive/simple-examples/working/write_3.c
index 15572577..3fce57cd 100644
--- a/src/example-archive/simple-examples/working/write_3.c
+++ b/src/example-archive/simple-examples/working/write_3.c
@@ -6,10 +6,26 @@ void write_3(int *cell1, int *cell2)
       cell1 == cell2;
     ensures 
       take Cell2Post = RW<int>(cell2);
-      Cell2Post == 8i32; @*/
+      Cell2Post == 8; @*/
 {
   *cell1 = 7;
+  #ifdef CN_INSTRUMENT
+  /*@ assert(*cell1 == 7 && *cell2 == 7); @*/
+  #else
   assert(*cell1 == 7 && *cell2 == 7);
+  #endif
   *cell2 = 8;
+  #ifdef CN_INSTRUMENT
+  /*@ assert(*cell1 == 8 && *cell2 == 8); @*/
+  #else
   assert(*cell1 == 8 && *cell2 == 8);
+  #endif
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x;
+  int *y = &x;
+  write_3(&x, y);
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/write_4.c b/src/example-archive/simple-examples/working/write_4.c
index 9971bda0..ea02ab62 100644
--- a/src/example-archive/simple-examples/working/write_4.c
+++ b/src/example-archive/simple-examples/working/write_4.c
@@ -9,9 +9,18 @@ void write_4()
     ensures
       take Cell1Post = RW<int>(cell1);
       take Cell2Post = RW<int>(cell2);
-      Cell1Post == 7i32;
-      Cell2Post == 8i32; @*/
+      Cell1Post == 7;
+      Cell2Post == 8; @*/
 {
   *cell1 = 7;
   *cell2 = 8;
 }
+
+int main(void)
+/*@ trusted; @*/
+{
+  int x, y;
+  // Need to initialise the cells for write_4's spec to read from them
+  cell1 = &x, cell2 = &y;
+  write_4();
+}
\ No newline at end of file
diff --git a/src/example-archive/simple-examples/working/write_5.c b/src/example-archive/simple-examples/working/write_5.c
index 9b27c5ff..46fc4426 100644
--- a/src/example-archive/simple-examples/working/write_5.c
+++ b/src/example-archive/simple-examples/working/write_5.c
@@ -3,12 +3,12 @@
 void write_5(int *pair)
 /*@ requires 
       take Cell1Pre = RW(pair);
-      take Cell2Pre = RW(pair + 1i32);
+      take Cell2Pre = RW(pair + 1);
     ensures 
       take Cell1Post = RW(pair);
-      take Cell2Post = RW(pair + 1i32); 
-      Cell1Post == 7i32; 
-      Cell2Post == 8i32; @*/
+      take Cell2Post = RW(pair + 1); 
+      Cell1Post == 7; 
+      Cell2Post == 8; @*/
 {
   pair[0] = 7;
   pair[1] = 8;
@@ -18,15 +18,26 @@ void write_5(int *pair)
 
 void write_5_alt(int *pair)
 /*@ requires 
-      take PairPre = each (i32 j; j == 0i32 || j == 1i32) {RW(pair + j)};
+      take PairPre = each (integer j; j == 0 || j == 1) {RW(pair + j)};
     ensures 
-      take PairPost = each (i32 j; j == 0i32 || j == 1i32) {RW(pair + j)}; 
-      PairPost[0i32] == 7i32; 
-      PairPost[1i32] == 8i32; 
+      take PairPost = each (integer j; j == 0 || j == 1) {RW(pair + j)}; 
+      PairPost[0] == 7; 
+      PairPost[1] == 8; 
       @*/
 {
-  /*@ focus RW<int>, 0i32; @*/
+  /*@ focus RW<int>, 0; @*/
   pair[0] = 7;
-  /*@ focus RW<int>, 1i32; @*/
+  /*@ focus RW<int>, 1; @*/
   pair[1] = 8;
 }
+
+void *cn_malloc(unsigned long size);
+
+int main(void)
+/*@ trusted; @*/
+{
+  int *pair = cn_malloc(sizeof(int) * 2);
+  write_5(pair);
+  int *pair2 = cn_malloc(sizeof(int) * 2);
+  write_5_alt(pair2);
+}
\ No newline at end of file
diff --git a/src/exercises/abs.c b/src/exercises/abs.c
index 79da4d60..e73ba012 100644
--- a/src/exercises/abs.c
+++ b/src/exercises/abs.c
@@ -1,7 +1,7 @@
 int abs (int x)
 /* --BEGIN-- */
 /*@ requires MINi32() < x;
-    ensures return == ((x >= 0i32) ? x : (0i32-x));
+    ensures return == ((x >= 0) ? x : (0-x));
 @*/
 /* --END-- */
 {
diff --git a/src/exercises/abs_mem.c b/src/exercises/abs_mem.c
index 3a188c3f..4460a90a 100644
--- a/src/exercises/abs_mem.c
+++ b/src/exercises/abs_mem.c
@@ -4,7 +4,7 @@ int abs_mem (int *p)
              MINi32() < x;
     ensures take x_post = RW<int>(p);
             x == x_post;
-            return == ((x >= 0i32) ? x : (0i32-x));
+            return == ((x >= 0) ? x : (0-x));
 @*/
 /* --END-- */
 {
diff --git a/src/exercises/abs_mem_struct.c b/src/exercises/abs_mem_struct.c
index 0bf68750..e58cd048 100644
--- a/src/exercises/abs_mem_struct.c
+++ b/src/exercises/abs_mem_struct.c
@@ -4,7 +4,7 @@ int abs_mem (int *p)
              MINi32() < x;
     ensures take x2 = RW<int>(p);
             x == x2;
-            return == ((x >= 0i32) ? x : (0i32-x));
+            return == ((x >= 0) ? x : (0-x));
 @*/
 /* --END-- */
 {
@@ -30,7 +30,7 @@ int abs_y (struct tuple *p)
              MINi32() < s.y;
     ensures  take s2 = RW(p);
              s == s2;
-             return == ((s.y >= 0i32) ? s.y : (0i32-s.y));
+             return == ((s.y >= 0) ? s.y : (0-s.y));
 @*/
 {
   return abs_mem(&p->y);
diff --git a/src/exercises/add_0.c b/src/exercises/add_0.c
index f0f52745..f286d606 100644
--- a/src/exercises/add_0.c
+++ b/src/exercises/add_0.c
@@ -1,7 +1,7 @@
 int add(int x, int y)
 /* --BEGIN-- */
-/*@ requires let Sum = (i64) x + (i64) y;
-             -2147483648i64 <= Sum; Sum <= 2147483647i64; @*/
+/*@ requires let Sum = x + y;
+             -2147483648 <= Sum; Sum <= 2147483647; @*/
 /* --END-- */
 {
   return x+y;
diff --git a/src/exercises/add_1.c b/src/exercises/add_1.c
index ac30ccc5..9269cd57 100644
--- a/src/exercises/add_1.c
+++ b/src/exercises/add_1.c
@@ -1,8 +1,8 @@
 int add(int x, int y)
 /* --BEGIN-- */
-/*@ requires let Sum = (i64) x + (i64) y;
-             -2147483648i64 <= Sum; Sum <= 2147483647i64;
-    ensures return == (i32) Sum;
+/*@ requires let Sum = x + y;
+             -2147483648 <= Sum; Sum <= 2147483647;
+    ensures return == Sum;
 @*/
 /* --END-- */
 {
diff --git a/src/exercises/add_2.c b/src/exercises/add_2.c
index 0afd69e0..f256434e 100644
--- a/src/exercises/add_2.c
+++ b/src/exercises/add_2.c
@@ -1,8 +1,8 @@
 int add(int x, int y)
 /* --BEGIN-- */
-/*@ requires let Sum = (i64) x + (i64) y;
-             (i64)MINi32() <= Sum; Sum <= (i64)MAXi32();
-    ensures return == (i32) Sum;
+/*@ requires let Sum = x + y;
+             MINi32() <= Sum; Sum <= MAXi32();
+    ensures return == Sum;
 @*/
 /* --END-- */
 {
diff --git a/src/exercises/add_read.c b/src/exercises/add_read.c
index bb93e867..cbe09e5c 100644
--- a/src/exercises/add_read.c
+++ b/src/exercises/add_read.c
@@ -1,6 +1,7 @@
 unsigned int add (unsigned int *p, unsigned int *q)
 /*@ requires take P = RW<unsigned int>(p);
              take Q = RW<unsigned int>(q);
+	     P + Q <= MAXu32();
     ensures take P_post = RW<unsigned int>(p);
             take Q_post = RW<unsigned int>(q);
             P == P_post && Q == Q_post;
diff --git a/src/exercises/array_init.c b/src/exercises/array_init.c
index c81a6006..a4755894 100644
--- a/src/exercises/array_init.c
+++ b/src/exercises/array_init.c
@@ -1,14 +1,14 @@
 void array_init (char *p, unsigned int n)
-/*@ requires take A = each(u32 i; i < n) { 
+/*@ requires take A = each(integer i; i < n) { 
                          RW<char>( array_shift<char>(p, i)) };
-    ensures  take A_post = each(u32 i; i < n) { 
+    ensures  take A_post = each(integer i; i < n) { 
                              RW<char>( array_shift<char>(p, i)) };
 @*/
 {
   unsigned int j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take Ai = each(u32 i; i < n) { 
+  /*@ inv take Ai = each(integer i; i < n) { 
                       RW<char>( array_shift<char>(p, i)) };
           {p} unchanged; 
           {n} unchanged;
diff --git a/src/exercises/array_init2.c b/src/exercises/array_init2.c
index a32c13dd..adb5fc93 100644
--- a/src/exercises/array_init2.c
+++ b/src/exercises/array_init2.c
@@ -1,16 +1,16 @@
 void array_init2 (char *p, unsigned int n)
-/*@ requires take A = each(u32 i; i < n) { 
+/*@ requires take A = each(integer i; 0 <= i && i < n) { 
                         W<char>( array_shift<char>(p, i)) };
-    ensures  take A_post = each(u32 i; i < n) { 
+    ensures  take A_post = each(integer i; 0 <= i && i < n) { 
                              RW<char>( array_shift<char>(p, i)) };
 @*/
 {
   unsigned int j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take Al = each(u32 i; i < j) { 
+  /*@ inv take Al = each(integer i; 0 <= i && i < j) { 
                       RW<char>( array_shift<char>(p, i)) };
-          take Ar = each(u32 i; j <= i && i < n) { 
+          take Ar = each(integer i; j <= i && i < n) { 
                       W<char>( array_shift<char>(p, i)) };
           {p} unchanged; {n} unchanged;
           j <= n;
diff --git a/src/exercises/array_init_rev.c b/src/exercises/array_init_rev.c
index 60b5bf06..03ede4cd 100644
--- a/src/exercises/array_init_rev.c
+++ b/src/exercises/array_init_rev.c
@@ -1,16 +1,16 @@
 void array_init_rev (char *p, unsigned int n)
-/*@ requires take A = each(u32 i; i < n) { 
+/*@ requires take A = each(integer i; i < n) { 
                         RW<char>( array_shift<char>(p, i)) };
-    ensures  take A_post = each(u32 i; i < n) { 
+    ensures  take A_post = each(integer i; i < n) { 
                              RW<char>( array_shift<char>(p, i)) };
 @*/
 {
   unsigned int j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take Al = each(u32 i; i < n-j) { 
+  /*@ inv take Al = each(integer i; i < n-j) { 
                       RW<char>( array_shift<char>(p, i)) };
-          take Ar = each(u32 i; n-j <= i && i < n) { 
+          take Ar = each(integer i; n-j <= i && i < n) { 
                       RW<char>( array_shift<char>(p, i)) };
           {p} unchanged; {n} unchanged;
           j <= n;
@@ -18,8 +18,8 @@ void array_init_rev (char *p, unsigned int n)
 /* --END-- */
   {
 /* --BEGIN-- */
-    /*@ focus RW<char>, n-(j+1u32); @*/
-    /*@ focus RW<char>, n-(j+1u32); @*/
+    /*@ focus RW<char>, n-(j+1); @*/
+    /*@ instantiate n-(j+1); @*/
 /* --END-- */
     p[n-(j+1)] = 0;
     j++;
diff --git a/src/exercises/array_load.c b/src/exercises/array_load.c
index 80805dda..f1efd5cf 100644
--- a/src/exercises/array_load.c
+++ b/src/exercises/array_load.c
@@ -1,12 +1,13 @@
 unsigned int read (unsigned int *p, unsigned int n, unsigned int i)
-/*@ requires take A = each(u32 j; j < n)
+/*@ requires take A = each(integer j; j < n)
                       { RW<unsigned int>(array_shift<unsigned int>(p,j)) };
              i < n; 
-    ensures take A_post = each(u32 j; j < n) 
+    ensures take A_post = each(integer j; j < n) 
                           { RW<unsigned int>(array_shift<unsigned int>(p,j)) };
             return == A[i];
 @*/
 {
   /*@ focus RW<unsigned int>, i; @*/
+  /*@ instantiate i; @*/
   return p[i];
 }
diff --git a/src/exercises/array_load2.c b/src/exercises/array_load2.c
index fdc98e88..617df702 100644
--- a/src/exercises/array_load2.c
+++ b/src/exercises/array_load2.c
@@ -1,11 +1,12 @@
 int read (int *p, int n, int i)
-/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { RW<int>(array_shift<int>(p,j)) };
-             0i32 <= i && i < n;
-    ensures take a2 = each(i32 j; 0i32 <= j && j < n) { RW<int>(array_shift<int>(p,j)) };
+/*@ requires take a1 = each(integer j; 0 <= j && j < n) { RW<int>(array_shift<int>(p,j)) };
+             0 <= i && i < n;
+    ensures take a2 = each(integer j; 0 <= j && j < n) { RW<int>(array_shift<int>(p,j)) };
             a1 == a2;
             return == a1[i];
 @*/
 {
   /*@ focus RW<int>, i; @*/
+  /*@ instantiate i; @*/
   return p[i];
 }
diff --git a/src/exercises/array_read_two.c b/src/exercises/array_read_two.c
index 8789bd22..5fe160d8 100644
--- a/src/exercises/array_read_two.c
+++ b/src/exercises/array_read_two.c
@@ -1,11 +1,12 @@
 unsigned int array_read_two (unsigned int *p, int n, int i, int j)
 /* --BEGIN-- */
-/*@ requires take A = each(i32 k; 0i32 <= k && k < n) { 
+/*@ requires take A = each(integer k; 0 <= k && k < n) { 
                         RW<unsigned int>(array_shift<unsigned int>(p,k)) };
-             0i32 <= i && i < n;
-             0i32 <= j && j < n;
+             0 <= i && i < n;
+             0 <= j && j < n;
              j != i;
-    ensures take A_post = each(i32 k; 0i32 <= k && k < n) { 
+	     A[i] + A[j] <= MAXu32();
+    ensures take A_post = each(integer k; 0 <= k && k < n) { 
                             RW<unsigned int>(array_shift<unsigned int>(p,k)) };
             A == A_post;
             return == A[i] + A[j];
@@ -14,10 +15,12 @@ unsigned int array_read_two (unsigned int *p, int n, int i, int j)
 {
 /* --BEGIN-- */
   /*@ focus RW<unsigned int>, i; @*/
+  /*@ instantiate i; @*/
 /* --END-- */
   unsigned int tmp1 = p[i];
 /* --BEGIN-- */
   /*@ focus RW<unsigned int>, j; @*/
+  /*@ instantiate j; @*/
 /* --END-- */
   unsigned int tmp2 = p[j];
   return (tmp1 + tmp2);
diff --git a/src/exercises/array_swap.c b/src/exercises/array_swap.c
index d54ef43a..35cb28bc 100644
--- a/src/exercises/array_swap.c
+++ b/src/exercises/array_swap.c
@@ -1,20 +1,22 @@
 void array_swap (int *p, int n, int i, int j)
 /* --BEGIN-- */
-/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { RW<int>(array_shift<int>(p,k)) };
-             0i32 <= i && i < n;
-             0i32 <= j && j < n;
+/*@ requires take a1 = each(integer k; 0 <= k && k < n) { RW<int>(array_shift<int>(p,k)) };
+             0 <= i && i < n;
+             0 <= j && j < n;
              j != i;
-    ensures take a2 = each(i32 k; 0i32 <= k && k < n) { RW<int>(array_shift<int>(p,k)) };
+    ensures take a2 = each(integer k; 0 <= k && k < n) { RW<int>(array_shift<int>(p,k)) };
             a2 == a1[i: a1[j], j: a1[i]];
 @*/
 /* --END-- */
 {
 /* --BEGIN-- */
   /*@ focus RW<int>, i; @*/
+  /*@ instantiate i; @*/
 /* --END-- */
   int tmp = p[i];
 /* --BEGIN-- */
   /*@ focus RW<int>, j; @*/
+  /*@ instantiate j; @*/
 /* --END-- */
   p[i] = p[j];
   p[j] = tmp;
diff --git a/src/exercises/bcp_framerule.c b/src/exercises/bcp_framerule.c
index d0a6caf3..4364ff94 100644
--- a/src/exercises/bcp_framerule.c
+++ b/src/exercises/bcp_framerule.c
@@ -1,7 +1,8 @@
 void incr_first (unsigned int *p, unsigned int *q)
 /*@ requires take pv = RW<unsigned int>(p);
+                  pv < MAXu32();
     ensures take pv_ = RW<unsigned int>(p);
-            pv_ == pv + 1u32;
+            pv_ == pv + 1;
 @*/
 {
   unsigned int n = *p;
@@ -11,10 +12,11 @@ void incr_first (unsigned int *p, unsigned int *q)
 
 void incr_first_frame (unsigned int *p, unsigned int *q)
 /*@ requires take pv = RW<unsigned int>(p);
+             pv < MAXu32();
              take qv = RW<unsigned int>(q);
     ensures take pv_ = RW<unsigned int>(p);
             take qv_ = RW<unsigned int>(q);
-            pv_ == pv + 1u32;
+            pv_ == pv + 1;
             qv_ == qv;
 @*/
 {
diff --git a/src/exercises/const_example.c b/src/exercises/const_example.c
deleted file mode 100644
index 2e192a23..00000000
--- a/src/exercises/const_example.c
+++ /dev/null
@@ -1,12 +0,0 @@
-#define CONST 1
-    /*@ function (i32) CONST () @*/
-    static int c_CONST() /*@ cn_function CONST; @*/ { return CONST; }
-
-int foo (int x)
-/*@
-  requires true;
-  ensures return == CONST();
-@*/
-{
-  return CONST;
-}
diff --git a/src/exercises/double_it.c b/src/exercises/double_it.c
index 7258d4c8..cd56ad74 100644
--- a/src/exercises/double_it.c
+++ b/src/exercises/double_it.c
@@ -1,6 +1,7 @@
 unsigned int double_it (unsigned int *p)
 /* --BEGIN-- */
 /*@ requires take P = RW<unsigned int>(p);
+             P + P <= MAXu32();
     ensures  take P_post = RW<unsigned int>(p);
              return == P + P;
              P_post == P;
diff --git a/src/exercises/five_six.c b/src/exercises/five_six.c
index 82ddf8ee..eb2d7f1d 100644
--- a/src/exercises/five_six.c
+++ b/src/exercises/five_six.c
@@ -3,7 +3,7 @@ unsigned int five_six(unsigned int *p, unsigned int *q)
 		     take Q = RW<unsigned int>(q);
     ensures  take P_post = RW<unsigned int>(p);
     		 take Q_post = RW<unsigned int>(q);
-             return == 5u32;
+             return == 5;
 @*/
 {
 	*p = 5;
diff --git a/src/exercises/id_by_div/id_by_div.fixed.c b/src/exercises/id_by_div/id_by_div.fixed.c
index aeafe018..6ab97ddd 100644
--- a/src/exercises/id_by_div/id_by_div.fixed.c
+++ b/src/exercises/id_by_div/id_by_div.fixed.c
@@ -1,6 +1,6 @@
 unsigned int id_by_div(unsigned int x)
-/*@ requires x % 2u32 == 0u32;
+/*@ requires rem(x, 2) == 0;
 	ensures return == x; @*/ 
 {
 	return (x / 2) * 2;
-}
\ No newline at end of file
+}
diff --git a/src/exercises/init_point.c b/src/exercises/init_point.c
index 640e0b77..35495505 100644
--- a/src/exercises/init_point.c
+++ b/src/exercises/init_point.c
@@ -1,7 +1,7 @@
 void zero (unsigned int *coord) 
 /*@ requires take Coord = RW<unsigned int>(coord);
     ensures take Coord_post = RW<unsigned int>(coord);
-            Coord_post == 0u32; @*/
+            Coord_post == 0; @*/
 {
   *coord = 0;
 }
@@ -11,8 +11,8 @@ struct point { unsigned int x; unsigned int y; };
 void init_point(struct point *p) 
 /*@ requires take P = RW<struct point>(p);
     ensures take P_post = RW<struct point>(p);
-            P_post.x == 0u32;
-            P_post.y == 0u32;
+            P_post.x == 0;
+            P_post.y == 0;
 @*/
 {
   zero(&p->x);
diff --git a/src/exercises/list/cn_types.h b/src/exercises/list/cn_types.h
index e294c6eb..b8a2ff8f 100644
--- a/src/exercises/list/cn_types.h
+++ b/src/exercises/list/cn_types.h
@@ -1,7 +1,7 @@
 /*@
 datatype List {
   Nil {},
-  Cons {i32 Head, datatype List Tail}
+  Cons {integer Head, datatype List Tail}
 }
 
 predicate [rec] (datatype List) SLList_At(pointer p) {
diff --git a/src/exercises/list/hdtl.h b/src/exercises/list/hdtl.h
index e36738ff..dbd13e2b 100644
--- a/src/exercises/list/hdtl.h
+++ b/src/exercises/list/hdtl.h
@@ -1,8 +1,8 @@
 /*@
-function (i32) Hd (datatype List L) {
+function (integer) Hd (datatype List L) {
   match L {
     Nil {} => {
-      0i32
+      0
     }
     Cons {Head : H, Tail : _} => {
       H
diff --git a/src/exercises/list/length.c b/src/exercises/list/length.c
index e7844ae0..429ef1f4 100644
--- a/src/exercises/list/length.c
+++ b/src/exercises/list/length.c
@@ -2,13 +2,13 @@
 
 /* --BEGIN-- */
 /*@
-function [rec] (u32) Length(datatype List L) {
+function [rec] (integer) Length(datatype List L) {
   match L {
     Nil {} => {
-      0u32
+      0
     }
     Cons {Head: H, Tail : T}  => {
-      1u32 + Length(T)
+      1 + Length(T)
     }
   }
 }
@@ -18,6 +18,7 @@ function [rec] (u32) Length(datatype List L) {
 unsigned int length (struct sllist *l)
 /* --BEGIN-- */
 /*@ requires take L = SLList_At(l);
+             Length(L) < MAXu32();
     ensures take L_post = SLList_At(l);
             L == L_post;
             return == Length(L);
diff --git a/src/exercises/list/rev_lemmas.h b/src/exercises/list/rev_lemmas.h
index 8e6dd044..1b7db8bb 100644
--- a/src/exercises/list/rev_lemmas.h
+++ b/src/exercises/list/rev_lemmas.h
@@ -3,7 +3,7 @@ lemma Append_Nil_RList (datatype List L1)
   requires true;
   ensures Append(L1, Nil{}) == L1;
 
-lemma Append_Cons_RList (datatype List L1, i32 X, datatype List L2)
+lemma Append_Cons_RList (datatype List L1, integer X, datatype List L2)
   requires true;
   ensures Append(L1, Cons {Head: X, Tail: L2})
           == Append(Snoc(L1, X), L2);
diff --git a/src/exercises/list/snoc.h b/src/exercises/list/snoc.h
index 97a27f77..7eb61ccb 100644
--- a/src/exercises/list/snoc.h
+++ b/src/exercises/list/snoc.h
@@ -1,5 +1,5 @@
 /*@
-function [rec] (datatype List) Snoc(datatype List Xs, i32 Y) {
+function [rec] (datatype List) Snoc(datatype List Xs, integer Y) {
   match Xs {
     Nil {} => {
       Cons {Head: Y, Tail: Nil{}}
diff --git a/src/exercises/queue/pop_lemma.h b/src/exercises/queue/pop_lemma.h
index ef76aaab..671dbf51 100644
--- a/src/exercises/queue/pop_lemma.h
+++ b/src/exercises/queue/pop_lemma.h
@@ -1,5 +1,5 @@
 /*@
-lemma snoc_facts (pointer front, pointer back, i32 x)
+lemma snoc_facts (pointer front, pointer back, integer x)
   requires
       take Q = QueueAux(front, back);
       take B = RW<struct queue_cell>(back);
diff --git a/src/exercises/queue/pop_unified.c b/src/exercises/queue/pop_unified.c
index 3ae33cbf..aaaba791 100644
--- a/src/exercises/queue/pop_unified.c
+++ b/src/exercises/queue/pop_unified.c
@@ -3,7 +3,7 @@
 /*@
 type_synonym result = { datatype List after, datatype List before }
 
-predicate (result) Queue_pop_lemma(pointer front, pointer back, i32 popped) {
+predicate (result) Queue_pop_lemma(pointer front, pointer back, integer popped) {
   if (is_null(front)) {
     return { after: Nil{}, before: Snoc(Nil{}, popped) };
   } else {
diff --git a/src/exercises/ref.h b/src/exercises/ref.h
index de69904b..572c5080 100644
--- a/src/exercises/ref.h
+++ b/src/exercises/ref.h
@@ -1,12 +1,12 @@
 extern unsigned int *refUnsignedInt (unsigned int v);
-/*@ spec refUnsignedInt(u32 v);
+/*@ spec refUnsignedInt(integer v);
     requires true;
     ensures take R = RW(return);
             R == v;
 @*/
 
 extern int *refInt (int v);
-/*@ spec refInt(i32 v);
+/*@ spec refInt(integer v);
     requires true;
     ensures take R = RW(return);
             R == v;
diff --git a/src/exercises/runway/funcs1.h b/src/exercises/runway/funcs1.h
index 2d2dd2c6..6b67fba8 100644
--- a/src/exercises/runway/funcs1.h
+++ b/src/exercises/runway/funcs1.h
@@ -9,13 +9,13 @@ struct State init()
 
 struct State increment_Plane_Counter(struct State s)
 /*@ requires valid_state(s);
-             0i32 <= s.Plane_Counter;
-             s.Plane_Counter <= 2i32;
+             0 <= s.Plane_Counter;
+             s.Plane_Counter <= 2;
              s.ModeA == ACTIVE() || s.ModeD == ACTIVE();
-             s.ModeA == ACTIVE() implies s.W_D > 0i32;
-             s.ModeD == ACTIVE() implies s.W_A > 0i32;
+             s.ModeA == ACTIVE() implies s.W_D > 0;
+             s.ModeD == ACTIVE() implies s.W_A > 0;
     ensures  valid_state(return);
-             s.Plane_Counter == return.Plane_Counter - 1i32;
+             s.Plane_Counter == return.Plane_Counter - 1;
              s.Runway_Time == return.Runway_Time;
              s.ModeA == return.ModeA;
              s.ModeD == return.ModeD;
@@ -31,7 +31,7 @@ struct State increment_Plane_Counter(struct State s)
 struct State reset_Plane_Counter(struct State s)
 /*@ requires valid_state(s);
     ensures  valid_state(return);
-             return.Plane_Counter == 0i32;
+             return.Plane_Counter == 0;
              s.Runway_Time == return.Runway_Time;
              s.ModeA == return.ModeA;
              s.ModeD == return.ModeD;
@@ -42,4 +42,4 @@ struct State reset_Plane_Counter(struct State s)
   struct State temp = s;
   temp.Plane_Counter = 0;
   return temp;
-}
\ No newline at end of file
+}
diff --git a/src/exercises/runway/funcs2.c b/src/exercises/runway/funcs2.c
index 2b0fd609..461f01a0 100644
--- a/src/exercises/runway/funcs2.c
+++ b/src/exercises/runway/funcs2.c
@@ -5,8 +5,8 @@
 struct State increment_Runway_Time(struct State s)
 /* --BEGIN-- */
 /*@ requires valid_state(s);
-             0i32 <= s.Runway_Time;
-             s.Runway_Time <= 4i32;
+             0 <= s.Runway_Time;
+             s.Runway_Time <= 4;
              s.ModeA == ACTIVE() || s.ModeD == ACTIVE();
     ensures  valid_state(return);
              s.Plane_Counter == return.Plane_Counter;
@@ -24,7 +24,7 @@ struct State reset_Runway_Time(struct State s)
 /* --BEGIN-- */
 /*@ requires valid_state(s);
     ensures  valid_state(return);
-             return.Runway_Time == 0i32;
+             return.Runway_Time == 0;
              s.ModeA == return.ModeA;
              s.ModeD == return.ModeD;
              s.W_A == return.W_A;
@@ -41,17 +41,17 @@ struct State reset_Runway_Time(struct State s)
 struct State arrive(struct State s)
 /* --BEGIN-- */
 /*@ requires valid_state(s);
-             s.ModeA == ACTIVE() && s.W_A >= 1i32;
-             s.Plane_Counter <= 2i32;
+             s.ModeA == ACTIVE() && s.W_A >= 1;
+             s.Plane_Counter <= 2;
     ensures  valid_state(return);
              s.Runway_Time == return.Runway_Time;
              s.ModeA == return.ModeA;
              s.ModeD == return.ModeD;
              s.W_D == return.W_D;
-             s.W_D == 0i32 
+             s.W_D == 0 
                implies s.Plane_Counter == return.Plane_Counter;
-             s.W_D > 0i32 
-               implies s.Plane_Counter == return.Plane_Counter - 1i32;
+             s.W_D > 0 
+               implies s.Plane_Counter == return.Plane_Counter - 1;
 @*/
 /* --END-- */
 {
@@ -66,8 +66,8 @@ struct State arrive(struct State s)
 struct State depart(struct State s)
 /* --BEGIN-- */
 /*@ requires valid_state(s);
-             s.ModeD == ACTIVE() && s.W_D >=1i32;
-             s.Plane_Counter <= 2i32;
+             s.ModeD == ACTIVE() && s.W_D >=1;
+             s.Plane_Counter <= 2;
     ensures  valid_state(return);
               s.Runway_Time == return.Runway_Time;
               s.ModeA == return.ModeA;
@@ -88,7 +88,7 @@ struct State switch_modes(struct State s)
 /* --BEGIN-- */
 /*@ requires valid_state(s);
              s.ModeA == ACTIVE() || s.ModeD == ACTIVE();
-             s.Plane_Counter == 0i32;
+             s.Plane_Counter == 0;
     ensures  valid_state(return);
              return.ModeA == ACTIVE() || return.ModeD == ACTIVE();
              return.ModeA == s.ModeD;
@@ -123,13 +123,13 @@ struct State switch_modes(struct State s)
 struct State tick(struct State s)
 /* --BEGIN-- */
 /*@ requires valid_state(s);
-             (i64) s.Plane_Counter < 2147483647i64;
-             (i64) s.W_A < 2147483647i64;
-             (i64) s.W_D < 2147483647i64;
+             s.Plane_Counter < 2147483647;
+             s.W_A < 2147483647;
+             s.W_D < 2147483647;
     ensures valid_state(return);
-            (s.W_A > 0i32 && s.W_D == 0i32 && s.Runway_Time == 0i32 
+            (s.W_A > 0 && s.W_D == 0 && s.Runway_Time == 0 
                implies return.ModeA == ACTIVE());
-            (s.W_D > 0i32 && s.W_A == 0i32 && s.Runway_Time == 0i32 
+            (s.W_D > 0 && s.W_A == 0 && s.Runway_Time == 0 
                implies return.ModeD == ACTIVE());
 @*/
 /* --END-- */
diff --git a/src/exercises/runway/state.h b/src/exercises/runway/state.h
index 4ec54041..6b08cbd4 100644
--- a/src/exercises/runway/state.h
+++ b/src/exercises/runway/state.h
@@ -1,12 +1,12 @@
 #define INACTIVE 0
-/*@ function (i32) INACTIVE() { 0i32 } @*/
+/*@ function (integer) INACTIVE() { 0 } @*/
 static int c_INACTIVE()
 /*@ requires true; 
     ensures return == INACTIVE(); @*/
 { return INACTIVE; }
 
 #define ACTIVE 1
-/*@ function (i32) ACTIVE() { 1i32 } @*/
+/*@ function (integer) ACTIVE() { 1 } @*/
 static int c_ACTIVE()
 /*@ requires true; 
     ensures return == ACTIVE(); @*/
diff --git a/src/exercises/runway/valid_state.h b/src/exercises/runway/valid_state.h
index b7e8b2e5..1694eb00 100644
--- a/src/exercises/runway/valid_state.h
+++ b/src/exercises/runway/valid_state.h
@@ -4,16 +4,16 @@ function (boolean) valid_state (struct State s) {
      (s.ModeD == INACTIVE() || s.ModeD == ACTIVE()) &&
      (s.ModeA == INACTIVE() || s.ModeD == INACTIVE()) &&
 
-     (s.W_A >= 0i32 && s.W_D >= 0i32) &&
-     (0i32 <= s.Runway_Time && s.Runway_Time <= 5i32) && 
-     (0i32 <= s.Plane_Counter && s.Plane_Counter <= 3i32) && 
+     (s.W_A >= 0 && s.W_D >= 0) &&
+     (0 <= s.Runway_Time && s.Runway_Time <= 5) && 
+     (0 <= s.Plane_Counter && s.Plane_Counter <= 3) && 
 
      (s.ModeA == INACTIVE() && s.ModeD == INACTIVE() 
-        implies s.Plane_Counter == 0i32) &&
-     (s.Runway_Time > 0i32 
+        implies s.Plane_Counter == 0) &&
+     (s.Runway_Time > 0 
         implies (s.ModeA == ACTIVE() || s.ModeD == ACTIVE())) &&
 
-     (s.Plane_Counter > 0i32 && s.ModeA == ACTIVE() implies s.W_D > 0i32) &&
-     (s.Plane_Counter > 0i32 && s.ModeD == ACTIVE() implies s.W_A > 0i32)
+     (s.Plane_Counter > 0 && s.ModeA == ACTIVE() implies s.W_D > 0) &&
+     (s.Plane_Counter > 0 && s.ModeD == ACTIVE() implies s.W_A > 0)
 }
 @*/
diff --git a/src/exercises/slf0_basic_incr.c b/src/exercises/slf0_basic_incr.c
index 7f8c0793..416c9ab4 100644
--- a/src/exercises/slf0_basic_incr.c
+++ b/src/exercises/slf0_basic_incr.c
@@ -1,7 +1,8 @@
 void incr (unsigned int *p)
 /*@ requires take P = RW<unsigned int>(p);
+             P < MAXu32();
     ensures take P_post = RW<unsigned int>(p);
-            P_post == P + 1u32;
+            P_post == P + 1;
 @*/
 {
   unsigned int n = *p;
diff --git a/src/exercises/slf0_basic_incr.signed.c b/src/exercises/slf0_basic_incr.signed.c
index e8f04e84..c3af5e1f 100644
--- a/src/exercises/slf0_basic_incr.signed.c
+++ b/src/exercises/slf0_basic_incr.signed.c
@@ -1,8 +1,8 @@
 void incr (int *p)
 /*@ requires take P = RW<int>(p);
-             ((i64) P) + 1i64 <= (i64) MAXi32();
+             P + 1 <= MAXi32();
     ensures take P_post = RW<int>(p);
-            P_post == P + 1i32;
+            P_post == P + 1;
 @*/
 {
   *p = *p+1;
diff --git a/src/exercises/slf10_basic_ref.c b/src/exercises/slf10_basic_ref.c
index a516bb74..443a7ab2 100644
--- a/src/exercises/slf10_basic_ref.c
+++ b/src/exercises/slf10_basic_ref.c
@@ -1,5 +1,5 @@
 extern unsigned int *refUnsignedInt (unsigned int v);
-/*@ spec refUnsignedInt(u32 v);
+/*@ spec refUnsignedInt(integer v);
     requires true;
     ensures take vr = RW(return);
             vr == v;
diff --git a/src/exercises/slf11_basic_ref_greater.c b/src/exercises/slf11_basic_ref_greater.c
index 7f7d1e4d..6bf20596 100644
--- a/src/exercises/slf11_basic_ref_greater.c
+++ b/src/exercises/slf11_basic_ref_greater.c
@@ -3,10 +3,11 @@
 unsigned int *ref_greater (unsigned int *p)
 /* --BEGIN-- */
 /*@ requires take n1 = RW(p);
+             n1 < MAXu32();
     ensures  take n2 = RW(p);
              take m2 = RW(return);
              n2 == n1;
-             m2 == n1 + 1u32;
+             m2 == n1 + 1;
 @*/
 /* --END-- */
 {
diff --git a/src/exercises/slf12_basic_ref_greater_abstract.c b/src/exercises/slf12_basic_ref_greater_abstract.c
index b057989f..fa32e59f 100644
--- a/src/exercises/slf12_basic_ref_greater_abstract.c
+++ b/src/exercises/slf12_basic_ref_greater_abstract.c
@@ -3,7 +3,7 @@
 unsigned int *ref_greater (unsigned int *p)
 /* --BEGIN-- */
 /*@ requires take n1 = RW(p);
-             n1 < n1 + 1u32;
+             n1 < MAXu32();
     ensures  take n2 = RW(p);
              take m2 = RW(return);
              n2 == n1;
diff --git a/src/exercises/slf16_basic_succ_using_incr.c b/src/exercises/slf16_basic_succ_using_incr.c
index cd0ac9a2..70b89e9a 100644
--- a/src/exercises/slf16_basic_succ_using_incr.c
+++ b/src/exercises/slf16_basic_succ_using_incr.c
@@ -3,7 +3,8 @@
 #include "slf0_basic_incr.c"
 
 unsigned int succ_using_incr (unsigned int n)
-/*@ ensures return == n + 1u32; @*/
+/*@ requires n < MAXu32();
+    ensures return == n + 1; @*/
 {
   unsigned int *p = refUnsignedInt(n);
   incr(p);
diff --git a/src/exercises/slf18_two_dice.c b/src/exercises/slf18_two_dice.c
index 04f11cdc..b21e1266 100644
--- a/src/exercises/slf18_two_dice.c
+++ b/src/exercises/slf18_two_dice.c
@@ -1,11 +1,11 @@
 unsigned int val_rand (unsigned int n);
-/*@ spec val_rand(u32 n);
-    requires n > 0u32;
-    ensures 0u32 <= return && return < n;
+/*@ spec val_rand(integer n);
+    requires n > 0;
+    ensures 0 <= return && return < n;
 @*/
 
 unsigned int two_dice ()
-/*@ ensures 2u32 <= return && return <= 12u32; @*/
+/*@ ensures 2 <= return && return <= 12; @*/
 {
   unsigned int n1 = val_rand (6);
   unsigned int n2 = val_rand (6);
diff --git a/src/exercises/slf1_basic_example_let.c b/src/exercises/slf1_basic_example_let.c
index fe53b6f1..f510e75e 100644
--- a/src/exercises/slf1_basic_example_let.c
+++ b/src/exercises/slf1_basic_example_let.c
@@ -1,5 +1,6 @@
 unsigned int example_let (unsigned int n) 
-/*@ ensures return == 2u32 * n;
+/*@ requires MINu32() < n && 2*n <= MAXu32();
+    ensures return == 2 * n;
 @*/
 {
   unsigned int a = n+1;
diff --git a/src/exercises/slf1_basic_example_let.signed.c b/src/exercises/slf1_basic_example_let.signed.c
index 44064ebd..68dc9781 100644
--- a/src/exercises/slf1_basic_example_let.signed.c
+++ b/src/exercises/slf1_basic_example_let.signed.c
@@ -1,9 +1,8 @@
 int doubled (int n)
 /* --BEGIN-- */
-/*@ requires let N = (i64) n;
-             (i64)MINi32() <= N - 1i64; N + 1i64 <= (i64)MAXi32();
-             (i64)MINi32() <= N + N; N + N <= (i64)MAXi32();
-    ensures return == n * 2i32;
+/*@ requires MINi32() <= n - 1; n + 1 <= MAXi32();
+             MINi32() <= n + n; n + n <= MAXi32();
+    ensures return == n * 2;
 @*/
 /* --END-- */
 {
diff --git a/src/exercises/slf2_basic_quadruple.c b/src/exercises/slf2_basic_quadruple.c
index 573eeb3b..58fa014d 100644
--- a/src/exercises/slf2_basic_quadruple.c
+++ b/src/exercises/slf2_basic_quadruple.c
@@ -1,5 +1,6 @@
 unsigned int quadruple (unsigned int n)
-/*@ ensures return == 4u32 * n; @*/
+/*@ requires 4 * n <= MAXu32();
+    ensures return == 4 * n; @*/
 {
   unsigned int m = n + n;
   return m + m;
diff --git a/src/exercises/slf2_basic_quadruple.signed.c b/src/exercises/slf2_basic_quadruple.signed.c
index 92e71f5d..a2241ccb 100644
--- a/src/exercises/slf2_basic_quadruple.signed.c
+++ b/src/exercises/slf2_basic_quadruple.signed.c
@@ -1,8 +1,7 @@
 int quadruple (int n)
 /* --BEGIN-- */
-/*@ requires let N = (i64) n;
-             (i64)MINi32() <= N * 4i64; N * 4i64 <= (i64)MAXi32();
-    ensures return == 4i32 * n;
+/*@ requires MINi32() <= n * 4; n * 4 <= MAXi32();
+    ensures return == 4 * n;
  @*/
 /* --END-- */
 {
diff --git a/src/exercises/slf3_basic_inplace_double.c b/src/exercises/slf3_basic_inplace_double.c
index 2e2a07b9..d43ff1a7 100644
--- a/src/exercises/slf3_basic_inplace_double.c
+++ b/src/exercises/slf3_basic_inplace_double.c
@@ -1,6 +1,7 @@
 void inplace_double (unsigned int *p)
 /* --BEGIN-- */
 /*@ requires take P = RW<unsigned int>(p);
+             P + P <= MAXu32();
     ensures  take P_post = RW<unsigned int>(p);
              P_post == P + P;
 @*/
diff --git a/src/exercises/slf4_basic_incr_two.c b/src/exercises/slf4_basic_incr_two.c
index ed1f7b36..bbaf95ab 100644
--- a/src/exercises/slf4_basic_incr_two.c
+++ b/src/exercises/slf4_basic_incr_two.c
@@ -3,10 +3,12 @@
 void incr_two (unsigned int *p, unsigned int *q)
 /*@ requires take n1 = RW(p);
              take m1 = RW(q);
+	     n1 < MAXu32();
+	     m1 < MAXu32();
     ensures take n2 = RW(p);
             take m2 = RW(q);
-            n2 == n1 + 1u32;
-            m2 == m1 + 1u32;
+            n2 == n1 + 1;
+            m2 == m1 + 1;
 @*/
 {
   incr(p);
diff --git a/src/exercises/slf6_basic_incr_two_aliased_call.c b/src/exercises/slf6_basic_incr_two_aliased_call.c
index e18e39db..16eb463b 100644
--- a/src/exercises/slf6_basic_incr_two_aliased_call.c
+++ b/src/exercises/slf6_basic_incr_two_aliased_call.c
@@ -3,9 +3,10 @@
 
 void incr_two (unsigned int *p, unsigned int *q)
 /*@ requires take n1 = RW(p);
+             n1 + 2 <= MAXu32();
              ptr_eq(q,p);
     ensures take n2 = RW(p);
-            n2 == n1 + 2u32;
+            n2 == n1 + 2;
 @*/
 {
   incr(p);
@@ -16,8 +17,9 @@ void incr_two (unsigned int *p, unsigned int *q)
 
 void aliased_call (unsigned int *p)
 /*@ requires take n1 = RW(p);
+             n1 + 2 <= MAXu32();
     ensures  take n2 = RW(p);
-             n2 == n1 + 2u32;
+             n2 == n1 + 2;
 @*/
 {
   incr_two(p, p);
diff --git a/src/exercises/slf7_basic_incr_first.c b/src/exercises/slf7_basic_incr_first.c
index 37f63d63..14d494a4 100644
--- a/src/exercises/slf7_basic_incr_first.c
+++ b/src/exercises/slf7_basic_incr_first.c
@@ -3,9 +3,10 @@
 void incr_first(unsigned int *p, unsigned int *q)
 /*@ requires take n1 = RW(p);
              take m1 = RW(q);
+             n1 < MAXu32();
     ensures  take n2 = RW(p);
              take m2 = RW(q);
-             n2 == n1 + 1u32;
+             n2 == n1 + 1;
              m2 == m1;
 @*/
 {
@@ -15,8 +16,9 @@ void incr_first(unsigned int *p, unsigned int *q)
 
 void incr_first_(unsigned int *p, unsigned int *q)
 /*@ requires take n1 = RW(p);
+             n1 < MAXu32();
     ensures  take n2 = RW(p);
-             n2 == n1 + 1u32;
+             n2 == n1 + 1;
 @*/
 {
   incr(p);
diff --git a/src/exercises/slf8_basic_transfer.c b/src/exercises/slf8_basic_transfer.c
index 409a0d0e..3ab8b866 100644
--- a/src/exercises/slf8_basic_transfer.c
+++ b/src/exercises/slf8_basic_transfer.c
@@ -2,10 +2,11 @@ void transfer (unsigned int *p, unsigned int *q)
 /* --BEGIN-- */
 /*@ requires take P = RW(p);
              take Q = RW(q);
+	     P+Q <= MAXu32();
     ensures  take P_post = RW(p);
              take Q_post = RW(q);
              P_post == P + Q;
-             Q_post == 0u32;
+             Q_post == 0;
 @*/
 /* --END-- */
 {
diff --git a/src/exercises/slf9_basic_transfer_aliased.c b/src/exercises/slf9_basic_transfer_aliased.c
index 53c4da63..45546e5d 100644
--- a/src/exercises/slf9_basic_transfer_aliased.c
+++ b/src/exercises/slf9_basic_transfer_aliased.c
@@ -2,7 +2,7 @@ void transfer (unsigned int *p, unsigned int *q)
 /*@ requires take n1 = RW(p);
              ptr_eq(p,q);
     ensures  take n2 = RW(p);
-             n2 == 0u32;
+             n2 == 0;
 @*/
 {
   unsigned int n = *p;
diff --git a/src/exercises/slf_incr2.verif.c b/src/exercises/slf_incr2.verif.c
index f6995983..44f20cc7 100644
--- a/src/exercises/slf_incr2.verif.c
+++ b/src/exercises/slf_incr2.verif.c
@@ -1,5 +1,5 @@
 /*@
-predicate { u32 P, u32 Q } TakeBoth (pointer p, pointer q)
+predicate { integer P, integer Q } TakeBoth (pointer p, pointer q)
 {
   if (ptr_eq(p,q)) {
     take PX = RW<unsigned int>(p);
@@ -15,9 +15,12 @@ predicate { u32 P, u32 Q } TakeBoth (pointer p, pointer q)
 
 void incr2(unsigned int *p, unsigned int *q)
 /*@ requires take PQ = TakeBoth(p,q);
+             (ptr_eq(p,q)) implies PQ.P+2 <= MAXu32();
+             (!ptr_eq(p,q)) implies PQ.P+1 <= MAXu32();
+             (!ptr_eq(p,q)) implies PQ.Q+1 <= MAXu32();
     ensures take PQ_post = TakeBoth(p,q);
-            PQ_post.P == (!ptr_eq(p,q) ? (PQ.P + 1u32) : (PQ.P + 2u32));
-            PQ_post.Q == (!ptr_eq(p,q) ? (PQ.Q + 1u32) : PQ_post.P);
+            PQ_post.P == (!ptr_eq(p,q) ? (PQ.P + 1) : (PQ.P + 2));
+            PQ_post.Q == (!ptr_eq(p,q) ? (PQ.Q + 1) : PQ_post.P);
 @*/
 {
   /*@ split_case ptr_eq(p,q); @*/
@@ -33,10 +36,12 @@ void call_both_better(unsigned int *p, unsigned int *q)
 /*@ requires take P = RW<unsigned int>(p);
              take Q = RW<unsigned int>(q);
              !ptr_eq(p,q);
+	     P < MAXu32() - 3;
+	     Q < MAXu32() - 1;
     ensures take P_post = RW<unsigned int>(p);
             take Q_post = RW<unsigned int>(q);
-            P_post == P + 3u32;
-            Q_post == Q + 1u32;
+            P_post == P + 3;
+            Q_post == Q + 1;
 @*/
 {
   incr2(p, q);
diff --git a/src/exercises/slf_incr2_alias.c b/src/exercises/slf_incr2_alias.c
index f50484ab..b4839acf 100644
--- a/src/exercises/slf_incr2_alias.c
+++ b/src/exercises/slf_incr2_alias.c
@@ -2,10 +2,12 @@
 void incr2a (unsigned int *p, unsigned int *q)
 /*@ requires take P = RW<unsigned int>(p);
              take Q = RW<unsigned int>(q);
+	     P < MAXu32();
+	     Q < MAXu32();
     ensures take P_post = RW<unsigned int>(p);
             take Q_post = RW<unsigned int>(q);
-            P_post == P + 1u32;
-            Q_post == Q + 1u32;
+            P_post == P + 1;
+            Q_post == Q + 1;
 @*/
 {
   unsigned int n = *p;
@@ -19,10 +21,11 @@ void incr2a (unsigned int *p, unsigned int *q)
 // Increment the same pointer twice
 void incr2b (unsigned int *p, unsigned int *q)
 /*@ requires take P = RW<unsigned int>(p);
+	     P+2 <= MAXu32();
              ptr_eq(q,p);
     ensures take P_post = RW<unsigned int>(p);
             ptr_eq(q,p);
-            P_post == P + 2u32;
+            P_post == P + 2;
 @*/
 {
   unsigned int n = *p;
@@ -36,10 +39,12 @@ void incr2b (unsigned int *p, unsigned int *q)
 void call_both (unsigned int *p, unsigned int *q)
 /*@ requires take pv = RW<unsigned int>(p);
              take qv = RW<unsigned int>(q);
+	     pv+3 <= MAXu32();
+	     qv+1 <= MAXu32();
     ensures take pv_ = RW<unsigned int>(p);
             take qv_ = RW<unsigned int>(q);
-            pv_ == pv + 3u32;
-            qv_ == qv + 1u32;
+            pv_ == pv + 3;
+            qv_ == qv + 1;
 @*/
 {
   incr2a(p, q);   // increment two different pointers
diff --git a/src/exercises/slf_incr2_noalias.c b/src/exercises/slf_incr2_noalias.c
index 91dedd2d..e4fa2dae 100644
--- a/src/exercises/slf_incr2_noalias.c
+++ b/src/exercises/slf_incr2_noalias.c
@@ -1,10 +1,12 @@
 void incr2a (unsigned int *p, unsigned int *q)
 /*@ requires take P = RW<unsigned int>(p);
              take Q = RW<unsigned int>(q);
+	     P < MAXu32();
+	     Q < MAXu32();
     ensures take P_post = RW<unsigned int>(p);
             take Q_post = RW<unsigned int>(q);
-            P_post == P + 1u32;
-            Q_post == Q + 1u32;
+            P_post == P + 1;
+            Q_post == Q + 1;
 @*/
 {
   unsigned int n = *p;
diff --git a/src/exercises/slf_length_acc.c b/src/exercises/slf_length_acc.c
index 19d92139..adb26f14 100644
--- a/src/exercises/slf_length_acc.c
+++ b/src/exercises/slf_length_acc.c
@@ -3,13 +3,13 @@
 #include "free.h"
 
 /*@
-function [rec] (u32) length(datatype List xs) {
+function [rec] (integer) length(datatype List xs) {
   match xs {
     Nil {} => {
-      0u32
+      0
     }
     Cons {Head: h, Tail: zs}  => {
-      1u32 + length(zs)
+      1 + length(zs)
     }
   }
 }
@@ -19,6 +19,7 @@ void IntList_length_acc_aux (struct sllist *xs, unsigned int *p)
 /* --BEGIN-- */
 /*@ requires take L1 = SLList_At(xs);
              take P = RW<unsigned int>(p);
+	     P + length(L1) <= MAXu32();
     ensures take L1_post = SLList_At(xs);
             take P_post = RW<unsigned int>(p);
             L1 == L1_post;
@@ -39,6 +40,7 @@ void IntList_length_acc_aux (struct sllist *xs, unsigned int *p)
 unsigned int IntList_length_acc (struct sllist *xs)
 /* --BEGIN-- */
 /*@ requires take Xs = SLList_At(xs);
+             length(Xs) <= MAXu32();
     ensures take Xs_post = SLList_At(xs);
             Xs == Xs_post;
             return == length(Xs);
diff --git a/src/exercises/slf_quadruple_mem.c b/src/exercises/slf_quadruple_mem.c
index dd7f8ea0..793e88d7 100644
--- a/src/exercises/slf_quadruple_mem.c
+++ b/src/exercises/slf_quadruple_mem.c
@@ -1,11 +1,10 @@
 int quadruple_mem (int *p)
 /* --BEGIN-- */
 /*@ requires take P = RW<int>(p);
-             let P64 = (i64) P;
-             (i64)MINi32() <= P64 * 4i64; P64 * 4i64 <= (i64)MAXi32();
+             MINi32() <= P * 4; P * 4 <= MAXi32();
     ensures take P_post = RW<int>(p);
             P_post == P;
-            return == 4i32 * P;
+            return == 4 * P;
  @*/
 /* --END-- */
 {
diff --git a/src/exercises/slf_ref_greater.c b/src/exercises/slf_ref_greater.c
index 34222015..3bdad2f8 100644
--- a/src/exercises/slf_ref_greater.c
+++ b/src/exercises/slf_ref_greater.c
@@ -3,7 +3,7 @@
 unsigned int *ref_greater_abstract (unsigned int *p)
 /* --BEGIN-- */
 /*@ requires take P = RW<unsigned int>(p);
-             P < 4294967295u32;
+             P < 4294967295;
     ensures take P_post = RW<unsigned int>(p);
             take R = RW<unsigned int>(return);
             P == P_post;
diff --git a/src/exercises/slf_sized_stack.c b/src/exercises/slf_sized_stack.c
index 5dd71af7..ec7c7bb7 100644
--- a/src/exercises/slf_sized_stack.c
+++ b/src/exercises/slf_sized_stack.c
@@ -8,7 +8,7 @@ struct sized_stack
 };
 
 /*@
-type_synonym SizedStack = {u32 Size, datatype List Data}
+type_synonym SizedStack = {integer Size, datatype List Data}
 
 predicate (SizedStack) SizedStack_At (pointer p) {
     take P = RW<struct sized_stack>(p);
@@ -34,7 +34,7 @@ spec free__sized_stack(pointer s);
 
 struct sized_stack *create()
 /*@ ensures take R = SizedStack_At(return);
-            R.Size == 0u32;
+            R.Size == 0;
 @*/
 {
   struct sized_stack *s = malloc__sized_stack();
@@ -61,6 +61,7 @@ void push(struct sized_stack *s, int x)
 /* FILL IN HERE */
 /* ---BEGIN--- */
 /*@ requires take S = SizedStack_At(s);
+             S.Size < MAXu32();
     ensures take S_post = SizedStack_At(s);
             S_post.Data == Cons {Head:x, Tail:S.Data};
 @*/
@@ -78,7 +79,7 @@ int pop(struct sized_stack *s)
 /* FILL IN HERE */
 /* ---BEGIN--- */
 /*@ requires take S = SizedStack_At(s);
-             S.Size > 0u32;
+             S.Size > 0;
     ensures  take S_post = SizedStack_At(s);
              S_post.Data == Tl(S.Data);
              return == Hd(S.Data);
@@ -88,7 +89,7 @@ int pop(struct sized_stack *s)
   struct sllist *data = s->data;
   /* ---BEGIN--- */
   /*@ unfold Length(S.Data); @*/
-  // from S.Size > 0u32 it follows that the 'else' branch is impossible
+  // from S.Size > 0 it follows that the 'else' branch is impossible
   /* ---END--- */
   if (data != 0)
   {
@@ -104,14 +105,14 @@ int pop(struct sized_stack *s)
 
 int top(struct sized_stack *s)
 /*@ requires take S = SizedStack_At(s);
-             S.Size > 0u32;
+             S.Size > 0;
     ensures  take S_post = SizedStack_At(s);
              S_post == S;
              return == Hd(S.Data);
 @*/
 {
   /*@ unfold Length(S.Data); @*/
-  // from S.Size > 0u32 it follows that the 'else' branch is impossible
+  // from S.Size > 0 it follows that the 'else' branch is impossible
   if (s->data != 0)
   {
     return (s->data)->head;
diff --git a/src/exercises/zero.c b/src/exercises/zero.c
index bcb45ce6..2a2ddee1 100644
--- a/src/exercises/zero.c
+++ b/src/exercises/zero.c
@@ -2,7 +2,7 @@ void zero (unsigned int *p)
 /* --BEGIN-- */
 /*@ requires take P = W<unsigned int>(p);
     ensures take P_post = RW<unsigned int>(p);
-            P_post == 0u32;
+            P_post == 0;
 @*/
 /* --END-- */
 {