From b85ff5f39ffb8f9e777f91d43626608be271df6a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 10 Apr 2026 08:40:06 +0000
Subject: [PATCH] Initialize nondet locals in regression tests

Prepares for --uninitialized-check becoming a default check.

Replace bare uninitialized local variable declarations with explicit
initialization in ~175 regression test files. These tests use
uninitialized locals as a shorthand for nondeterministic values
(e.g., int x; __CPROVER_assume(x > 0);). This is undefined behaviour in
C that we used to tolerate in CBMC. Once we enable --uninitialized-check
by default, however, those would have become (unwanted) verification
failures.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 regression/cbmc/ACSL/operators.c              |  4 +-
 regression/cbmc/Array_Pointer3/main.c         |  2 +-
 regression/cbmc/Array_UF1/main.c              |  3 +-
 regression/cbmc/Array_UF2/main.c              |  3 +-
 regression/cbmc/Array_operations1/main.c      |  2 +-
 regression/cbmc/Array_operations2/main.c      |  2 +-
 regression/cbmc/Array_operations4/main.c      |  2 +-
 regression/cbmc/Associativity1/main.c         | 11 +--
 regression/cbmc/BV_Arithmetic6/main.c         |  4 +-
 regression/cbmc/Bitfields1/main.c             |  3 +-
 regression/cbmc/Bitfields2/main.c             |  3 +-
 regression/cbmc/Boolean_Guards1/main.c        | 14 ++--
 regression/cbmc/Computed-Goto1/main.c         |  2 +-
 regression/cbmc/Ellipsis2/main.c              |  4 +-
 regression/cbmc/Empty_struct1/main.c          |  2 +-
 regression/cbmc/End_thread1/main.c            |  2 +-
 regression/cbmc/Fixedbv4/main.c               |  3 +-
 regression/cbmc/Fixedbv5/main.c               | 13 +--
 regression/cbmc/Fixedbv6/main.c               |  3 +-
 regression/cbmc/Float-equality1/main.c        |  3 +-
 regression/cbmc/Float-equality2/main.c        |  4 +-
 regression/cbmc/Float-flags-no-simp1/main.c   |  2 +-
 regression/cbmc/Float-flags-simp1/main.c      |  2 +-
 regression/cbmc/Float-no-simp2/main.c         |  2 +-
 regression/cbmc/Float-no-simp4/main.c         | 10 +--
 regression/cbmc/Float-no-simp5/main.c         |  2 +-
 regression/cbmc/Float-rounding2/main.c        |  4 +-
 regression/cbmc/Float12/main.c                |  4 +-
 regression/cbmc/Float20/main.c                |  6 +-
 regression/cbmc/Float22/main.c                | 30 +++----
 regression/cbmc/Float23/main.c                |  2 +-
 regression/cbmc/Float4/main.c                 |  2 +-
 regression/cbmc/Float5/main.c                 |  2 +-
 regression/cbmc/Float6/main.c                 |  3 +-
 regression/cbmc/Float8/main.c                 |  2 +-
 regression/cbmc/Function1/main.c              |  8 +-
 regression/cbmc/Function4/main.c              |  2 +-
 regression/cbmc/Function_Pointer10/main.c     |  2 +-
 regression/cbmc/Function_Pointer2/main.c      |  2 +-
 regression/cbmc/Function_Pointer6/main.c      |  2 +-
 regression/cbmc/Malloc11/main.c               |  4 +-
 regression/cbmc/Malloc13/main.c               |  2 +-
 regression/cbmc/Malloc17/main.c               |  6 +-
 regression/cbmc/Malloc18/main.c               |  2 +-
 regression/cbmc/Malloc9/main.c                |  2 +-
 regression/cbmc/Minisat_Simp1/main.c          |  2 +-
 regression/cbmc/Mod2/main.c                   |  2 +-
 regression/cbmc/Pointer1/main.c               |  2 +-
 regression/cbmc/Pointer15/main.c              |  2 +-
 regression/cbmc/Pointer25/main.c              |  2 +-
 regression/cbmc/Pointer26/main.c              |  2 +-
 regression/cbmc/Pointer9/main.c               |  2 +-
 regression/cbmc/Pointer_Arithmetic11/main.c   |  2 +-
 regression/cbmc/Pointer_array8/main.c         |  2 +-
 regression/cbmc/Pointer_byte_extract4/main.c  | 82 +++++++++----------
 regression/cbmc/Pointer_comparison3/main.c    |  2 +-
 regression/cbmc/Pointer_difference2/main.c    |  4 +-
 .../cbmc/Quantifiers-expr-cleaning/main.c     |  2 +-
 .../Quantifiers-simplify/rewrite_exists.c     |  2 +-
 .../Quantifiers-statement-expression3/main.c  |  2 +-
 regression/cbmc/Recursion2/main.c             |  2 +-
 regression/cbmc/String8/main.c                |  2 +-
 .../String_Abstraction14/pass-in-implicit.c   |  2 +-
 .../cbmc/String_Abstraction15/pass-in.c       |  2 +-
 regression/cbmc/String_Abstraction18/strcpy.c |  2 +-
 .../cbmc/String_Abstraction21/strcpy2.c       |  2 +-
 regression/cbmc/String_Abstraction22/main.c   |  2 +-
 regression/cbmc/Struct_Initialization2/main.c |  2 +-
 regression/cbmc/Struct_Initialization5/main.c |  3 +-
 regression/cbmc/Struct_Propagation1/main.c    |  2 +-
 regression/cbmc/Typecast1/main.c              |  2 +-
 regression/cbmc/Unbounded_Array1/main.c       |  4 +-
 regression/cbmc/Unbounded_Array5/main.c       |  2 +-
 regression/cbmc/Undefined_Shift1/main.c       |  4 +-
 regression/cbmc/array-tests/uf-always.c       |  4 +-
 regression/cbmc/array-tests/zero-sized.c      |  2 +-
 regression/cbmc/atomic_X_fetch-1/main.c       | 10 +--
 regression/cbmc/atomic_fetch_X-1/main.c       |  2 +-
 .../cbmc/aws-byte-buf-regression/main.c       |  2 +-
 regression/cbmc/big-endian-array1/main.c      |  2 +-
 regression/cbmc/bounds_check1/main.c          | 10 ++-
 regression/cbmc/byte_update11/main.c          |  2 +-
 regression/cbmc/byte_update12/main.c          |  2 +-
 regression/cbmc/byte_update15/main.c          |  2 +-
 regression/cbmc/byte_update16/main.c          |  2 +-
 regression/cbmc/byte_update17/main.c          |  2 +-
 regression/cbmc/byte_update18/main.c          |  2 +-
 regression/cbmc/clang_builtins/bitreverse.c   |  8 +-
 regression/cbmc/clang_builtins/rotate.c       | 16 ++--
 .../cbmc/condition-propagation-4/test.c       |  2 +-
 regression/cbmc/divide-by-one-simplify/main.c |  2 +-
 regression/cbmc/dynamic_size1/stack_object.c  |  2 +-
 regression/cbmc/dynamic_sizeof1/main.c        |  2 +-
 regression/cbmc/enum9/main.c                  |  7 +-
 .../cbmc/equality_through_array1/main.c       |  4 +-
 .../cbmc/equality_through_array2/main.c       |  4 +-
 .../cbmc/equality_through_array3/main.c       |  4 +-
 .../cbmc/equality_through_array4/main.c       |  2 +-
 .../cbmc/equality_through_array5/main.c       |  2 +-
 .../cbmc/equality_through_array6/main.c       |  2 +-
 .../equality_through_array_of_struct1/main.c  |  2 +-
 .../equality_through_array_of_struct2/main.c  |  2 +-
 .../equality_through_array_of_struct3/main.c  |  2 +-
 .../equality_through_array_of_struct4/main.c  |  2 +-
 .../cbmc/equality_through_struct1/main.c      |  2 +-
 .../cbmc/equality_through_struct2/main.c      |  2 +-
 .../cbmc/equality_through_struct3/main.c      |  2 +-
 .../cbmc/equality_through_struct4/main.c      |  2 +-
 .../main.c                                    |  2 +-
 .../main.c                                    |  2 +-
 .../cbmc/equality_through_union1/main.c       | 16 ++--
 .../cbmc/equality_through_union2/main.c       | 18 ++--
 .../cbmc/equality_through_union3/main.c       | 24 +++---
 regression/cbmc/exit1/main.c                  |  2 +-
 regression/cbmc/field-sensitivity15/main.c    |  2 +-
 regression/cbmc/field-sensitivity16/main.c    |  2 +-
 regression/cbmc/gcc_switch_case_range1/main.c |  2 +-
 regression/cbmc/gcc_switch_case_range2/main.c |  2 +-
 regression/cbmc/gcc_vector1/main.c            |  3 +-
 regression/cbmc/goto1/main.c                  |  2 +-
 regression/cbmc/goto2/main.c                  |  2 +-
 regression/cbmc/guard1/main.c                 |  9 +-
 regression/cbmc/havoc_object1/main.c          |  2 +-
 regression/cbmc/if1/main.c                    |  2 +-
 regression/cbmc/if4/main.c                    |  2 +-
 .../main.c                                    |  2 +-
 .../main.c                                    |  2 +-
 .../cbmc/lhs-pointer-aliases-constant/test.c  |  2 +-
 regression/cbmc/little-endian-array1/main.c   |  2 +-
 regression/cbmc/no-propagation/main.c         |  2 +-
 regression/cbmc/null7/main.c                  |  2 +-
 regression/cbmc/overflow/leftshift_overflow.c |  2 +-
 .../cbmc/overflow/signed_multiplication1.c    |  2 +-
 .../cbmc/overflow/signed_subtraction1.c       |  2 +-
 .../cbmc/pointer-predicates/at_bounds1.c      |  2 +-
 regression/cbmc/pragma_cprover1/main.c        |  2 +-
 regression/cbmc/pragma_cprover2/main.c        |  2 +-
 regression/cbmc/pragma_cprover_enable1/main.c |  2 +-
 regression/cbmc/pragma_cprover_enable2/main.c |  2 +-
 regression/cbmc/r_w_ok1/main.c                |  2 +-
 regression/cbmc/r_w_ok7/main.c                |  4 +-
 regression/cbmc/return4/main.c                |  2 +-
 regression/cbmc/runtime-profiling/main.c      |  2 +-
 regression/cbmc/sat-solver-warning/test.c     |  2 +-
 regression/cbmc/simplify-array-size/main.c    |  2 +-
 regression/cbmc/struct1/main.c                |  3 +-
 regression/cbmc/struct3/main.c                | 19 +++--
 regression/cbmc/struct7/main.c                |  2 +-
 regression/cbmc/struct8/main.c                |  3 +-
 regression/cbmc/switch1/main.c                |  2 +-
 regression/cbmc/switch2/main.c                |  2 +-
 regression/cbmc/switch4/main.c                |  2 +-
 regression/cbmc/sync_X_and_fetch-1/main.c     |  2 +-
 regression/cbmc/sync_bool_compare-1/main.c    |  3 +-
 regression/cbmc/sync_fetch_and_X-1/main.c     |  2 +-
 regression/cbmc/sync_val_compare-1/main.c     |  3 +-
 regression/cbmc/uniform_array1/main.c         |  2 +-
 regression/cbmc/uninterpreted_function/uf2.c  |  2 +-
 regression/cbmc/union17/main.c                |  2 +-
 regression/cbmc/union3/main.c                 |  2 +-
 regression/cbmc/unwind_counters4/main.c       |  4 +-
 regression/cbmc/void_pointer3/main.c          |  3 +-
 162 files changed, 342 insertions(+), 308 deletions(-)

diff --git a/regression/cbmc/ACSL/operators.c b/regression/cbmc/ACSL/operators.c
index 518485fcc95..79525746ef4 100644
--- a/regression/cbmc/ACSL/operators.c
+++ b/regression/cbmc/ACSL/operators.c
@@ -1,6 +1,6 @@
 void boolean()
 {
-  __CPROVER_bool a, b;
+  __CPROVER_bool a = __VERIFIER_nondet__Bool(), b = __VERIFIER_nondet__Bool();
   __CPROVER_assert((a ≡ b) == (a == b), "≡");
   __CPROVER_assert((a ≢ b) == (a != b), "≢");
   __CPROVER_assert((a ⇒ b) == (!a || b), "⇒");
@@ -13,7 +13,7 @@ void boolean()
 
 void relations()
 {
-  int a, b;
+  int a = __VERIFIER_nondet_int(), b = __VERIFIER_nondet_int();
   __CPROVER_assert((a ≥ b) == (a >= b), "≥");
   __CPROVER_assert((a ≤ b) == (a <= b), "≤");
   __CPROVER_assert((a ≡ b) == (a == b), "≡");
diff --git a/regression/cbmc/Array_Pointer3/main.c b/regression/cbmc/Array_Pointer3/main.c
index bb7376a9b9c..2ed8ae927a1 100644
--- a/regression/cbmc/Array_Pointer3/main.c
+++ b/regression/cbmc/Array_Pointer3/main.c
@@ -62,7 +62,7 @@ int f(int j, int k)
 
 int main()
 {
-  int x, y;
+  int x = __VERIFIER_nondet_int(), y = __VERIFIER_nondet_int();
   __CPROVER_assume(x > y);
   __CPROVER_assume(x >= 0);
   __CPROVER_assume((y > 15) && (y < 18));
diff --git a/regression/cbmc/Array_UF1/main.c b/regression/cbmc/Array_UF1/main.c
index 64742bcd719..ea71a718362 100644
--- a/regression/cbmc/Array_UF1/main.c
+++ b/regression/cbmc/Array_UF1/main.c
@@ -1,7 +1,8 @@
 int main()
 {
   int a[10], b[10];
-  int x, y, z;
+  int x = __VERIFIER_nondet_int(), y = __VERIFIER_nondet_int(),
+      z = __VERIFIER_nondet_int();
   __CPROVER_assume(2 <= y && y <= 4);
   __CPROVER_assume(6 <= z && z <= 8);
   b[y] = x;
diff --git a/regression/cbmc/Array_UF2/main.c b/regression/cbmc/Array_UF2/main.c
index e3ddf0d1d64..6e84ce0c9d8 100644
--- a/regression/cbmc/Array_UF2/main.c
+++ b/regression/cbmc/Array_UF2/main.c
@@ -1,7 +1,8 @@
 int main()
 {
   int a[4], b[4];
-  int x, y, z;
+  int x = __VERIFIER_nondet_int(), y = __VERIFIER_nondet_int(),
+      z = __VERIFIER_nondet_int();
   __CPROVER_assume(1 <= y && y <= 3);
   __CPROVER_assume(0 <= z && z <= 2);
   b[y] = x;
diff --git a/regression/cbmc/Array_operations1/main.c b/regression/cbmc/Array_operations1/main.c
index f4d405bb981..b9abfcd175e 100644
--- a/regression/cbmc/Array_operations1/main.c
+++ b/regression/cbmc/Array_operations1/main.c
@@ -2,7 +2,7 @@ void test_equal()
 {
   char array1[100], array2[100];
   _Bool cmp;
-  int index;
+  int index = __VERIFIER_nondet_int();
 
   cmp = __CPROVER_array_equal(array1, array2);
 
diff --git a/regression/cbmc/Array_operations2/main.c b/regression/cbmc/Array_operations2/main.c
index 2e11a014cfa..cdaf6a97e89 100644
--- a/regression/cbmc/Array_operations2/main.c
+++ b/regression/cbmc/Array_operations2/main.c
@@ -11,7 +11,7 @@ int main()
 {
   my_struct arr[3] = {0};
   char *ptr = &(arr[1].c[2]);
-  int offset;
+  int offset = __VERIFIER_nondet_int();
   __CPROVER_assume(offset < 1 && offset > -1);
   void *ptr_plus = ptr + offset;
   char nondet[3];
diff --git a/regression/cbmc/Array_operations4/main.c b/regression/cbmc/Array_operations4/main.c
index 18cb51e1ebf..08140f5e6d7 100644
--- a/regression/cbmc/Array_operations4/main.c
+++ b/regression/cbmc/Array_operations4/main.c
@@ -3,7 +3,7 @@ int main()
   char source[8];
   int int_source[2];
   int target[4];
-  int n;
+  int n = __VERIFIER_nondet_int();
   if(n >= 0 && n < 3)
   {
     __CPROVER_array_replace(&target[n], source);
diff --git a/regression/cbmc/Associativity1/main.c b/regression/cbmc/Associativity1/main.c
index 905a37f3d4f..f79edf8f466 100644
--- a/regression/cbmc/Associativity1/main.c
+++ b/regression/cbmc/Associativity1/main.c
@@ -1,11 +1,12 @@
 #include <assert.h>
 
 int main (void) {
-	int x;
+  int x = __VERIFIER_nondet_int();
 
-	while ((x + 1) -x != 1) {
-		assert(0);
-	}
+  while((x + 1) - x != 1)
+  {
+    assert(0);
+  }
 
-	return 0;
+  return 0;
 }
diff --git a/regression/cbmc/BV_Arithmetic6/main.c b/regression/cbmc/BV_Arithmetic6/main.c
index d971a119fd0..e5e2eb6a5a1 100644
--- a/regression/cbmc/BV_Arithmetic6/main.c
+++ b/regression/cbmc/BV_Arithmetic6/main.c
@@ -1,7 +1,7 @@
 int main()
 {
   {
-    unsigned i, j, k, l;
+    unsigned i, j, k = __VERIFIER_nondet_unsigned(), l;
 
     j=k;
     i=j/2;
@@ -15,7 +15,7 @@ int main()
   }
 
   {
-    signed int i, j, k, l;
+    signed int i, j, k = __VERIFIER_nondet_signed_int(), l;
 
     // shifting rounds into the wrong direction
     __CPROVER_assume(!(k&1));
diff --git a/regression/cbmc/Bitfields1/main.c b/regression/cbmc/Bitfields1/main.c
index 670e4166809..8ccba093ac0 100644
--- a/regression/cbmc/Bitfields1/main.c
+++ b/regression/cbmc/Bitfields1/main.c
@@ -30,7 +30,8 @@ struct bft {
 };
 
 int main() {
-  struct bft bf;
+  struct bft nondet_bft(void);
+  struct bft bf = nondet_bft();
 
   assert(bf.a<=7);
   assert(bf.b<=1);
diff --git a/regression/cbmc/Bitfields2/main.c b/regression/cbmc/Bitfields2/main.c
index 4322e6aa4f9..827e2a114be 100644
--- a/regression/cbmc/Bitfields2/main.c
+++ b/regression/cbmc/Bitfields2/main.c
@@ -40,7 +40,8 @@ unsigned foo(union U u, struct S0 s)
 int main()
 {
   struct S0 main_s = { 0, 1, 2, 3, 4, 5, 6, 7, 8 };
-  union U main_u;
+  union U nondet_U(void);
+  union U main_u = nondet_U();
 
   assert(8==foo(main_u, main_s));
 
diff --git a/regression/cbmc/Boolean_Guards1/main.c b/regression/cbmc/Boolean_Guards1/main.c
index 14f125ab4ad..3c8ab91a2eb 100644
--- a/regression/cbmc/Boolean_Guards1/main.c
+++ b/regression/cbmc/Boolean_Guards1/main.c
@@ -1,18 +1,20 @@
-int main() {
-  unsigned x;
-  int i;
+int main()
+{
+  unsigned x = __VERIFIER_nondet_unsigned();
+  int i = __VERIFIER_nondet_int();
   int a[100];
+  __CPROVER_havoc_object(a);
 
   // this is guaranteed not to be a buffer overflow
-  if(x<100 && a[x])
+  if(x < 100 && a[x])
   {
     i++;
   }
 
-  __CPROVER_assume(i<100);
+  __CPROVER_assume(i < 100);
 
   // this is guaranteed not to be a buffer underflow
-  if(i>=0 && a[i])
+  if(i >= 0 && a[i])
   {
     i++;
   }
diff --git a/regression/cbmc/Computed-Goto1/main.c b/regression/cbmc/Computed-Goto1/main.c
index 0991d3ebd5f..3910704d78c 100644
--- a/regression/cbmc/Computed-Goto1/main.c
+++ b/regression/cbmc/Computed-Goto1/main.c
@@ -1,7 +1,7 @@
 int main()
 {
   static void *table[] = {&&l0, &&l1, &&l2};
-  int in, out;
+  int in = __VERIFIER_nondet_int(), out;
 
   if(in>=0 && in<=2)
   {
diff --git a/regression/cbmc/Ellipsis2/main.c b/regression/cbmc/Ellipsis2/main.c
index 0c206b81369..b98fe8235b3 100644
--- a/regression/cbmc/Ellipsis2/main.c
+++ b/regression/cbmc/Ellipsis2/main.c
@@ -7,8 +7,8 @@ int foo(int a, ...)
 
 int main()
 {
-  char c;
-  long l;
+  char c = __VERIFIER_nondet_char();
+  long l = __VERIFIER_nondet_long();
 
   if(c<l)
     l=foo(c, c);
diff --git a/regression/cbmc/Empty_struct1/main.c b/regression/cbmc/Empty_struct1/main.c
index b1d7a0b781d..dbb6f49cc48 100644
--- a/regression/cbmc/Empty_struct1/main.c
+++ b/regression/cbmc/Empty_struct1/main.c
@@ -7,7 +7,7 @@ struct empty
 int main()
 {
   struct empty e1, e2, e3;
-  _Bool b, c=b;
+  _Bool b = __VERIFIER_nondet__Bool(), c = b;
   e1=e2;
   if(b)
     e3=e2;
diff --git a/regression/cbmc/End_thread1/main.c b/regression/cbmc/End_thread1/main.c
index 661ae211e95..f3295ac2405 100644
--- a/regression/cbmc/End_thread1/main.c
+++ b/regression/cbmc/End_thread1/main.c
@@ -10,7 +10,7 @@ void pthread_exit(void *value_ptr);
 
 int main()
 {
-  int i;
+  int i = __VERIFIER_nondet_int();
 
   if(i == 100)
   {
diff --git a/regression/cbmc/Fixedbv4/main.c b/regression/cbmc/Fixedbv4/main.c
index d8079138627..a76c2bde563 100644
--- a/regression/cbmc/Fixedbv4/main.c
+++ b/regression/cbmc/Fixedbv4/main.c
@@ -4,7 +4,8 @@ typedef __CPROVER_fixedbv[32][16] fbvt;
 
 int main()
 {
-  fbvt f;
+  fbvt nondet_fbvt(void);
+  fbvt f = nondet_fbvt();
 
   // addition
   assert(100.0+10==110);
diff --git a/regression/cbmc/Fixedbv5/main.c b/regression/cbmc/Fixedbv5/main.c
index 059d29bccd0..0535ed7329f 100644
--- a/regression/cbmc/Fixedbv5/main.c
+++ b/regression/cbmc/Fixedbv5/main.c
@@ -1,11 +1,12 @@
 int main()
 {
   typedef __CPROVER_fixedbv[32][16] ft;
-  ft a, b;
+  ft nondet_ft(void);
+  ft a = nondet_ft(), b;
 
-  __CPROVER_assume(a==1 || a==(ft)0.5 || a==2 || a==3 || a==(ft)0.25);
-  b=a;
-  a/=2;
-  a*=2;
-  __CPROVER_assert(a==b, "fixedbv div works");
+  __CPROVER_assume(a == 1 || a == (ft)0.5 || a == 2 || a == 3 || a == (ft)0.25);
+  b = a;
+  a /= 2;
+  a *= 2;
+  __CPROVER_assert(a == b, "fixedbv div works");
 }
diff --git a/regression/cbmc/Fixedbv6/main.c b/regression/cbmc/Fixedbv6/main.c
index ebbad13d9c5..a55b15ff0f9 100644
--- a/regression/cbmc/Fixedbv6/main.c
+++ b/regression/cbmc/Fixedbv6/main.c
@@ -23,7 +23,8 @@ int main()
   assert(!((fbvt)-2.0>=(fbvt)-1.0));
 
   // variables
-  fbvt a, b, _a=a, _b=b;
+  fbvt nondet_fbvt(void);
+  fbvt a = nondet_fbvt(), b = nondet_fbvt(), _a = a, _b = b;
   __CPROVER_assume(a==1 && b==2);
 
   assert(a!=b);
diff --git a/regression/cbmc/Float-equality1/main.c b/regression/cbmc/Float-equality1/main.c
index a6d8205d1ab..e019388d4aa 100644
--- a/regression/cbmc/Float-equality1/main.c
+++ b/regression/cbmc/Float-equality1/main.c
@@ -2,7 +2,8 @@
 
 void main()
 {
-  double a, b, c;
+  double a = __VERIFIER_nondet_double(), b = __VERIFIER_nondet_double(),
+         c = __VERIFIER_nondet_double();
   __CPROVER_assume(a + b > c);
 #ifdef EQUALITY
   double x = a, y = b, z = c;
diff --git a/regression/cbmc/Float-equality2/main.c b/regression/cbmc/Float-equality2/main.c
index 3cd42cd8a3f..b3678e6613f 100644
--- a/regression/cbmc/Float-equality2/main.c
+++ b/regression/cbmc/Float-equality2/main.c
@@ -3,8 +3,8 @@
 
 int main()
 {
-  float a;
-  float b;
+  float a = __VERIFIER_nondet_float();
+  float b = __VERIFIER_nondet_float();
   // We could do "if (isnormal(a) && isnormal(b))", but __CPROVER_isnanf(a+b)
   // will permit solving this entirely via the simplifier, if, and only if, the
   // equality is successfully simplified (despite the different order of
diff --git a/regression/cbmc/Float-flags-no-simp1/main.c b/regression/cbmc/Float-flags-no-simp1/main.c
index 693981e9889..7b58d6b512b 100644
--- a/regression/cbmc/Float-flags-no-simp1/main.c
+++ b/regression/cbmc/Float-flags-no-simp1/main.c
@@ -4,7 +4,7 @@
 
 int main()
 {
-  double d;
+  double d = __VERIFIER_nondet_double();
 
 #ifndef _MSC_VER
 
diff --git a/regression/cbmc/Float-flags-simp1/main.c b/regression/cbmc/Float-flags-simp1/main.c
index 693981e9889..7b58d6b512b 100644
--- a/regression/cbmc/Float-flags-simp1/main.c
+++ b/regression/cbmc/Float-flags-simp1/main.c
@@ -4,7 +4,7 @@
 
 int main()
 {
-  double d;
+  double d = __VERIFIER_nondet_double();
 
 #ifndef _MSC_VER
 
diff --git a/regression/cbmc/Float-no-simp2/main.c b/regression/cbmc/Float-no-simp2/main.c
index 4914f3863ab..f35ecd7ebfb 100644
--- a/regression/cbmc/Float-no-simp2/main.c
+++ b/regression/cbmc/Float-no-simp2/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  double f, f2;
+  double f, f2 = __VERIFIER_nondet_double();
   // the following rely on f not being a NaN
   __CPROVER_assume(!__CPROVER_isnand(f2));
   __CPROVER_assume(__CPROVER_isfinited(f2));
diff --git a/regression/cbmc/Float-no-simp4/main.c b/regression/cbmc/Float-no-simp4/main.c
index 00041a6b944..df6f8ddfd6e 100644
--- a/regression/cbmc/Float-no-simp4/main.c
+++ b/regression/cbmc/Float-no-simp4/main.c
@@ -2,33 +2,33 @@
 
 int main()
 {
-  double d1, _d1;
+  double d1, _d1 = __VERIFIER_nondet_double();
   d1=_d1;
   __CPROVER_assume(__CPROVER_isnormald(d1));
   assert(!__CPROVER_isnand(d1));
   assert(!__CPROVER_isinfd(d1));
   assert(__CPROVER_isfinited(d1));
 
-  double d2, _d2;
+  double d2, _d2 = __VERIFIER_nondet_double();
   d2=_d2;
   __CPROVER_assume(__CPROVER_isinfd(d2));
   assert(!__CPROVER_isnormald(d2));
   assert(!__CPROVER_isnand(d2));
 
-  double d3, _d3;
+  double d3, _d3 = __VERIFIER_nondet_double();
   d3=_d3;
   __CPROVER_assume(__CPROVER_isnand(d3));
   assert(!__CPROVER_isnormald(d3));
   assert(!__CPROVER_isinfd(d3));
   assert(d3!=d3);
 
-  double d4, _d4;
+  double d4, _d4 = __VERIFIER_nondet_double();
   d4=_d4;
   __CPROVER_assume(__CPROVER_isfinited(d4));
   assert(!__CPROVER_isnand(d4));
   assert(!__CPROVER_isinfd(d4));
 
-  double d5, _d5;
+  double d5, _d5 = __VERIFIER_nondet_double();
   d5=_d5;
   __CPROVER_assume(!__CPROVER_isnand(d5) && !__CPROVER_isinfd(d5));
   assert(__CPROVER_isfinited(d5));
diff --git a/regression/cbmc/Float-no-simp5/main.c b/regression/cbmc/Float-no-simp5/main.c
index 7f4b1ed44a7..fefe8d8f5b0 100644
--- a/regression/cbmc/Float-no-simp5/main.c
+++ b/regression/cbmc/Float-no-simp5/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  double a, b;
+  double a = __VERIFIER_nondet_double(), b = __VERIFIER_nondet_double();
 
   union {
     double f;
diff --git a/regression/cbmc/Float-rounding2/main.c b/regression/cbmc/Float-rounding2/main.c
index a73715a6c5f..fe9058fb471 100644
--- a/regression/cbmc/Float-rounding2/main.c
+++ b/regression/cbmc/Float-rounding2/main.c
@@ -6,7 +6,7 @@ int main()
   // examples of constants that previously exhibited wrong behaviour
   union U
   {
-    double d;
+    double d = __VERIFIER_nondet_double();
     uint64_t b;
   };
   union U u = {
@@ -15,7 +15,7 @@ int main()
     .b = 0b0000000000000000000000000000001111111111111111111111111000000000};
   double d = u.d;
 #else
-  double d;
+  double d = __VERIFIER_nondet_double();
 #endif
   float f;
   if(d > 0.0 && d < 1.0)
diff --git a/regression/cbmc/Float12/main.c b/regression/cbmc/Float12/main.c
index 3b88b9d576f..05189be7045 100644
--- a/regression/cbmc/Float12/main.c
+++ b/regression/cbmc/Float12/main.c
@@ -1,8 +1,8 @@
 int main()
 {
-  float f;
+  float f = __VERIFIER_nondet_float();
   double d;
-  unsigned char x;
+  unsigned char x = __VERIFIER_nondet_char();
 
   d=f;
 
diff --git a/regression/cbmc/Float20/main.c b/regression/cbmc/Float20/main.c
index 5b1c69fe151..b7905c7beda 100644
--- a/regression/cbmc/Float20/main.c
+++ b/regression/cbmc/Float20/main.c
@@ -42,13 +42,13 @@ void bugCasting (double d) {
 }
 
 int main (void) {
-  float f;
+  float f = __VERIFIER_nondet_float();
   bug(f);
 
-  float g;
+  float g = __VERIFIER_nondet_float();
   bugBrokenOut(g);
 
-  double d;
+  double d = __VERIFIER_nondet_double();
   bugCasting(d);
 
   return 1;
diff --git a/regression/cbmc/Float22/main.c b/regression/cbmc/Float22/main.c
index f2ab9bf4382..4d83b3de7a6 100644
--- a/regression/cbmc/Float22/main.c
+++ b/regression/cbmc/Float22/main.c
@@ -25,35 +25,35 @@ typedef union _ieee754_float {
 
 
 float returnsField (uint32_t index) {
-    ieee754_float c;
+  ieee754_float c;
 
-    c.ieee.negative = index & 0x1;
-    c.ieee.exponent = 0;
-    c.ieee.mantissa = 0;
+  c.ieee.negative = index & 0x1;
+  c.ieee.exponent = 0;
+  c.ieee.mantissa = 0;
 
-    return c.f;
+  return c.f;
 }
 
 ieee754_float returnsStructure (uint32_t index) {
-    ieee754_float c;
+  ieee754_float c;
 
-    c.ieee.negative = index & 0x1;
-    c.ieee.exponent = 0;
-    c.ieee.mantissa = 0;
+  c.ieee.negative = index & 0x1;
+  c.ieee.exponent = 0;
+  c.ieee.mantissa = 0;
 
-    return c;
+  return c;
 }
 
 
 void testOne (void) {
-   ieee754_float f1, f2;
+  ieee754_float f1, f2;
 
-   f1 = returnsStructure(0);
-   f2 = returnsStructure(1);
+  f1 = returnsStructure(0);
+  f2 = returnsStructure(1);
 
-   assert(f1.ieee.negative != f2.ieee.negative);
+  assert(f1.ieee.negative != f2.ieee.negative);
 
-   return;
+  return;
 }
 
 
diff --git a/regression/cbmc/Float23/main.c b/regression/cbmc/Float23/main.c
index 874812c5399..237985a7552 100644
--- a/regression/cbmc/Float23/main.c
+++ b/regression/cbmc/Float23/main.c
@@ -1,5 +1,5 @@
 int main()
 {
-  float a, b;
+  float a = __VERIFIER_nondet_float(), b = __VERIFIER_nondet_float();
   __CPROVER_assert((a>b)==(a-b>0), "theorem");
 }
diff --git a/regression/cbmc/Float4/main.c b/regression/cbmc/Float4/main.c
index 4b3fd112caa..d77b8c54889 100644
--- a/regression/cbmc/Float4/main.c
+++ b/regression/cbmc/Float4/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  double f, f2;
+  double f, f2 = __VERIFIER_nondet_double();
   // the following rely on f not being a NaN or Infinity
   __CPROVER_assume(!__CPROVER_isnand(f2));
   __CPROVER_assume(!__CPROVER_isinfd(f2));
diff --git a/regression/cbmc/Float5/main.c b/regression/cbmc/Float5/main.c
index f35749769ef..e121b7ac800 100644
--- a/regression/cbmc/Float5/main.c
+++ b/regression/cbmc/Float5/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  float a, b;
+  float a = __VERIFIER_nondet_float(), b;
 
   __CPROVER_assume(a==1 || a==0.5 || a==2 || a==3 || a==0.1);
   b=a;
diff --git a/regression/cbmc/Float6/main.c b/regression/cbmc/Float6/main.c
index f72d72c6975..204e2e15d95 100644
--- a/regression/cbmc/Float6/main.c
+++ b/regression/cbmc/Float6/main.c
@@ -21,7 +21,8 @@ int main()
   assert(!(-2.0>=-1.0));
 
   // variables
-  float a, b, _a=a, _b=b;
+  float a = __VERIFIER_nondet_float(), b = __VERIFIER_nondet_float(), _a = a,
+        _b = b;
   __CPROVER_assume(a==1 && b==2);
 
   assert(a!=b);
diff --git a/regression/cbmc/Float8/main.c b/regression/cbmc/Float8/main.c
index f8f94c5f5cf..212c04bcede 100644
--- a/regression/cbmc/Float8/main.c
+++ b/regression/cbmc/Float8/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  double d, q, r;
+  double d, q = __VERIFIER_nondet_double(), r;
   __CPROVER_assume(__CPROVER_isfinited(q));
   d=q;
   r=d+0;
diff --git a/regression/cbmc/Function1/main.c b/regression/cbmc/Function1/main.c
index c39666b9903..e09675291cc 100644
--- a/regression/cbmc/Function1/main.c
+++ b/regression/cbmc/Function1/main.c
@@ -8,10 +8,10 @@ int f(int);
 int a[1];
 
 int main() {
-	int x, y;
+  int x, y = __VERIFIER_nondet_int();
 
-	a[0] = y;
-	a[0] = f(a[0]);
+  a[0] = y;
+  a[0] = f(a[0]);
 
-	assert(a[0] == y+1);
+  assert(a[0] == y + 1);
 }
diff --git a/regression/cbmc/Function4/main.c b/regression/cbmc/Function4/main.c
index dfdd644b79b..0c06c83fd0f 100644
--- a/regression/cbmc/Function4/main.c
+++ b/regression/cbmc/Function4/main.c
@@ -2,7 +2,7 @@ int nondet_int();
 
 int f1()
 {
-  int ret;
+  int ret = __VERIFIER_nondet_int();
   return ret;
 }
 
diff --git a/regression/cbmc/Function_Pointer10/main.c b/regression/cbmc/Function_Pointer10/main.c
index e974ca00403..eefcd1675a9 100644
--- a/regression/cbmc/Function_Pointer10/main.c
+++ b/regression/cbmc/Function_Pointer10/main.c
@@ -4,7 +4,7 @@ void fun(int a)
 
 int test1()
 {
-  char i;
+  char i = __VERIFIER_nondet_char();
   void (*fp)()=fun;
   // this requires a type conversion for i
   fp(i);
diff --git a/regression/cbmc/Function_Pointer2/main.c b/regression/cbmc/Function_Pointer2/main.c
index ee419e426d9..f56935d4ac5 100644
--- a/regression/cbmc/Function_Pointer2/main.c
+++ b/regression/cbmc/Function_Pointer2/main.c
@@ -13,7 +13,7 @@ void g(int garg)
 int main()
 {
   void (*p)(int);
-  __CPROVER_bool c;
+  __CPROVER_bool c = __VERIFIER_nondet___CPROVER_bool();
 
   p=c?f:g;
 
diff --git a/regression/cbmc/Function_Pointer6/main.c b/regression/cbmc/Function_Pointer6/main.c
index afb9a644d97..fa464d0ad42 100644
--- a/regression/cbmc/Function_Pointer6/main.c
+++ b/regression/cbmc/Function_Pointer6/main.c
@@ -18,7 +18,7 @@ int main(void)
 {
   int (*ppp)();
   struct S * ps = (struct S *) malloc(sizeof(struct S));
-  int x, y;
+  int x = __VERIFIER_nondet_int(), y;
 
   ps->func = x?ten:twenty;
 
diff --git a/regression/cbmc/Malloc11/main.c b/regression/cbmc/Malloc11/main.c
index 796446efe34..27480ecdcfb 100644
--- a/regression/cbmc/Malloc11/main.c
+++ b/regression/cbmc/Malloc11/main.c
@@ -2,10 +2,10 @@
 
 int main()
 {
-  int n;
+  int n = __VERIFIER_nondet_int();
   int x;
   int *a;
-  _Bool nondet;
+  _Bool nondet = __VERIFIER_nondet__Bool();
 
   __CPROVER_assume(n <= 10);
 
diff --git a/regression/cbmc/Malloc13/main.c b/regression/cbmc/Malloc13/main.c
index 0c39afb2cca..99902293743 100644
--- a/regression/cbmc/Malloc13/main.c
+++ b/regression/cbmc/Malloc13/main.c
@@ -1,7 +1,7 @@
 void *malloc(__CPROVER_size_t);
 
 int main(int argc, char* argv[]) {
-  unsigned short len;
+  unsigned short len = __VERIFIER_nondet_short();
   char * str;
   __CPROVER_assume(len > 0);
   str = malloc(len);
diff --git a/regression/cbmc/Malloc17/main.c b/regression/cbmc/Malloc17/main.c
index 192ed892ef7..55f2e13d150 100644
--- a/regression/cbmc/Malloc17/main.c
+++ b/regression/cbmc/Malloc17/main.c
@@ -1,6 +1,6 @@
 unsigned char* init1()
 {
-  unsigned long size;
+  unsigned long size = __VERIFIER_nondet_long();
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
@@ -14,7 +14,7 @@ unsigned char* init1()
 
 unsigned char* init2()
 {
-  unsigned long size;
+  unsigned long size = __VERIFIER_nondet_long();
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
@@ -28,7 +28,7 @@ unsigned char* init2()
 
 unsigned char* init3()
 {
-  unsigned long size;
+  unsigned long size = __VERIFIER_nondet_long();
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
diff --git a/regression/cbmc/Malloc18/main.c b/regression/cbmc/Malloc18/main.c
index 88dd8de1e25..7b09d55b9f6 100644
--- a/regression/cbmc/Malloc18/main.c
+++ b/regression/cbmc/Malloc18/main.c
@@ -1,6 +1,6 @@
 unsigned char* init()
 {
-  unsigned long buffer_size;
+  unsigned long buffer_size = __VERIFIER_nondet_long();
   if(buffer_size!=1) return 0;
 
   unsigned char* buffer=__CPROVER_allocate(buffer_size, 0);
diff --git a/regression/cbmc/Malloc9/main.c b/regression/cbmc/Malloc9/main.c
index da6028eea66..c882539aa0d 100644
--- a/regression/cbmc/Malloc9/main.c
+++ b/regression/cbmc/Malloc9/main.c
@@ -17,7 +17,7 @@ struct S2
 
 int main(void)
 {
-  _Bool b;
+  _Bool b = __VERIFIER_nondet__Bool();
 
   if(b)
   {
diff --git a/regression/cbmc/Minisat_Simp1/main.c b/regression/cbmc/Minisat_Simp1/main.c
index c704d4db878..92354004108 100644
--- a/regression/cbmc/Minisat_Simp1/main.c
+++ b/regression/cbmc/Minisat_Simp1/main.c
@@ -3,7 +3,7 @@ int isnan(double);
 
 int main()
 {
-  double my_d, dabs;
+  double my_d = __VERIFIER_nondet_double(), dabs;
 
   __CPROVER_assume(!isnan(my_d));
 
diff --git a/regression/cbmc/Mod2/main.c b/regression/cbmc/Mod2/main.c
index 13c715cb409..c45b00306c6 100644
--- a/regression/cbmc/Mod2/main.c
+++ b/regression/cbmc/Mod2/main.c
@@ -13,7 +13,7 @@ static int
 
 int main()
 {
- int a, b;
+ int a = __VERIFIER_nondet_int(), b = __VERIFIER_nondet_int();
 #ifdef __CPROVER__
  __CPROVER_assume(a==1);
  __CPROVER_assume(b==-2);
diff --git a/regression/cbmc/Pointer1/main.c b/regression/cbmc/Pointer1/main.c
index e5f44733be9..77ef8e8ad89 100644
--- a/regression/cbmc/Pointer1/main.c
+++ b/regression/cbmc/Pointer1/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int a, b, c, *p;
+  int a, b, c = __VERIFIER_nondet_int(), *p;
 
   if(c)
     p = &a;
diff --git a/regression/cbmc/Pointer15/main.c b/regression/cbmc/Pointer15/main.c
index 20913566930..5bcabb1c7e5 100644
--- a/regression/cbmc/Pointer15/main.c
+++ b/regression/cbmc/Pointer15/main.c
@@ -2,7 +2,7 @@ int main()
 {
   const void *p;
   int *q;
-  int c;
+  int c = __VERIFIER_nondet_int();
 
   p = (c ? p : 0);
 
diff --git a/regression/cbmc/Pointer25/main.c b/regression/cbmc/Pointer25/main.c
index d9903727dc4..7d12062c08d 100644
--- a/regression/cbmc/Pointer25/main.c
+++ b/regression/cbmc/Pointer25/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int x;
+  int x = __VERIFIER_nondet_int();
   void *p;
 
   // from integer 0 to NULL
diff --git a/regression/cbmc/Pointer26/main.c b/regression/cbmc/Pointer26/main.c
index 8804c864a6f..42e743e0a1c 100644
--- a/regression/cbmc/Pointer26/main.c
+++ b/regression/cbmc/Pointer26/main.c
@@ -3,7 +3,7 @@ int main()
   unsigned int *p = (unsigned int *)0xdeadbeef;
   assert(p != 0);
 
-  int zero;
+  int zero = __VERIFIER_nondet_int();
   __CPROVER_assume(zero == 0);
   unsigned int *q = (unsigned int *)zero;
   assert(q == 0);
diff --git a/regression/cbmc/Pointer9/main.c b/regression/cbmc/Pointer9/main.c
index 90915e79dae..c060860b572 100644
--- a/regression/cbmc/Pointer9/main.c
+++ b/regression/cbmc/Pointer9/main.c
@@ -16,7 +16,7 @@ void f1(int *px)
 
 main()
 {
-  int flag;
+  int flag = __VERIFIER_nondet_int();
   int *ref = NULL;
   int x = 0;
   st1.x = 0;
diff --git a/regression/cbmc/Pointer_Arithmetic11/main.c b/regression/cbmc/Pointer_Arithmetic11/main.c
index c1b2df18592..e42f20c367c 100644
--- a/regression/cbmc/Pointer_Arithmetic11/main.c
+++ b/regression/cbmc/Pointer_Arithmetic11/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int i, ii;
+  int i, ii = __VERIFIER_nondet_int();
   int data=0;
   char *p=(char *)&data;
   i=ii;
diff --git a/regression/cbmc/Pointer_array8/main.c b/regression/cbmc/Pointer_array8/main.c
index af34389773c..bdd81164bcd 100644
--- a/regression/cbmc/Pointer_array8/main.c
+++ b/regression/cbmc/Pointer_array8/main.c
@@ -16,6 +16,6 @@ int main()
   arrvec A;
   arrvec *x = &A;
   __CPROVER_assume(x->vec[1].data[0] < 42);
-  unsigned k;
+  unsigned k = __VERIFIER_nondet_unsigned();
   __CPROVER_assert(k != 2 || ((int *)x)[k] < 42, "");
 }
diff --git a/regression/cbmc/Pointer_byte_extract4/main.c b/regression/cbmc/Pointer_byte_extract4/main.c
index fe43ff4cb7f..75392aac7f1 100644
--- a/regression/cbmc/Pointer_byte_extract4/main.c
+++ b/regression/cbmc/Pointer_byte_extract4/main.c
@@ -16,45 +16,45 @@ struct list_head gl_list = { &gl_list, &gl_list };
 
 int main()
 {
-  _Bool maybe_dynamic;
-
-  struct node X;
-  struct node *N = maybe_dynamic ? malloc(sizeof(struct node)) : &X;
-  if (!N)
-    return 1;
-
-  N->value = 42;
-	gl_list.prev=&N->linkage;
-	N->linkage.next=&gl_list;
-	N->linkage.prev=&gl_list;
-	gl_list.next=&N->linkage;
-  // we have:
-  // gl_list.prev=&D->linkage;
-  // D->linkage.next=&gl_list
-  // D->linkage.prev=&gl_list;
-  // gl_list.next=&D->linkage;
-
-	N->nested.next = &(N->nested);
-  N->nested.prev = &(N->nested);
-
-  const struct list_head *head=&gl_list;
-
-  // go one step backward
-  head = head->prev;
-  // we have:
-  // head=&D->linkage
-
-  // resolve root
-  const struct node *node =
-    (struct node *) ((char *)(head) -
-                     (unsigned long)(&((struct node *)0)->linkage));
-  // we have:
-  // node=&D (==&D->value)
-  __CPROVER_assert(node == N, "");
-  __CPROVER_assert(head == N->linkage.next->prev, "");
-  __CPROVER_assert(head == N->linkage.prev->next, "");
-  __CPROVER_assert(head == node->linkage.next->prev, "");
-  __CPROVER_assert(head == node->linkage.prev->next, "");
-
-  return 0;
+    _Bool maybe_dynamic = __VERIFIER_nondet__Bool();
+
+    struct node X;
+    struct node *N = maybe_dynamic ? malloc(sizeof(struct node)) : &X;
+    if(!N)
+      return 1;
+
+    N->value = 42;
+    gl_list.prev = &N->linkage;
+    N->linkage.next = &gl_list;
+    N->linkage.prev = &gl_list;
+    gl_list.next = &N->linkage;
+    // we have:
+    // gl_list.prev=&D->linkage;
+    // D->linkage.next=&gl_list
+    // D->linkage.prev=&gl_list;
+    // gl_list.next=&D->linkage;
+
+    N->nested.next = &(N->nested);
+    N->nested.prev = &(N->nested);
+
+    const struct list_head *head = &gl_list;
+
+    // go one step backward
+    head = head->prev;
+    // we have:
+    // head=&D->linkage
+
+    // resolve root
+    const struct node *node =
+      (struct node
+         *)((char *)(head) - (unsigned long)(&((struct node *)0)->linkage));
+    // we have:
+    // node=&D (==&D->value)
+    __CPROVER_assert(node == N, "");
+    __CPROVER_assert(head == N->linkage.next->prev, "");
+    __CPROVER_assert(head == N->linkage.prev->next, "");
+    __CPROVER_assert(head == node->linkage.next->prev, "");
+    __CPROVER_assert(head == node->linkage.prev->next, "");
+
+    return 0;
 }
diff --git a/regression/cbmc/Pointer_comparison3/main.c b/regression/cbmc/Pointer_comparison3/main.c
index 4ed0f75c2dd..4f0cf797fab 100644
--- a/regression/cbmc/Pointer_comparison3/main.c
+++ b/regression/cbmc/Pointer_comparison3/main.c
@@ -13,7 +13,7 @@ int main()
 
   assert(p1 != p2);
 
-  _Bool nondet;
+  _Bool nondet = __VERIFIER_nondet__Bool();
   // In the current implementation, CBMC always produces "false" for a
   // comparison over different objects. This could change at any time, which
   // would require updating this test.
diff --git a/regression/cbmc/Pointer_difference2/main.c b/regression/cbmc/Pointer_difference2/main.c
index 6342893ab64..f75e235295c 100644
--- a/regression/cbmc/Pointer_difference2/main.c
+++ b/regression/cbmc/Pointer_difference2/main.c
@@ -6,7 +6,7 @@ int main()
   __CPROVER_assert(&array[0] - &array[2] == -2, "correct");
 
   int diff = array - other_array;
-  _Bool nondet;
+  _Bool nondet = __VERIFIER_nondet__Bool();
   if(nondet)
     __CPROVER_assert(diff != 42, "undefined behavior");
   else
@@ -21,7 +21,7 @@ int main()
   __CPROVER_assert(p - &array[0] == 4, "end plus one works");
   __CPROVER_assert(p - &array[0] != 3, "end plus one works");
   ++p;
-  _Bool nondet_branch;
+  _Bool nondet_branch = __VERIFIER_nondet__Bool();
   if(nondet_branch)
     __CPROVER_assert(p - &array[0] == 5, "end plus 2 is nondet");
   else
diff --git a/regression/cbmc/Quantifiers-expr-cleaning/main.c b/regression/cbmc/Quantifiers-expr-cleaning/main.c
index 55ca455b210..eb5f6f030da 100644
--- a/regression/cbmc/Quantifiers-expr-cleaning/main.c
+++ b/regression/cbmc/Quantifiers-expr-cleaning/main.c
@@ -8,7 +8,7 @@ int main()
 
   // make value sets produce a derefd_pointer object for ((const char*)p)[i]
   // below
-  _Bool nondet;
+  _Bool nondet = __VERIFIER_nondet__Bool();
   int *p = nondet ? &x : &y;
 
   // clang-format off
diff --git a/regression/cbmc/Quantifiers-simplify/rewrite_exists.c b/regression/cbmc/Quantifiers-simplify/rewrite_exists.c
index bab785f868f..b37bb480369 100644
--- a/regression/cbmc/Quantifiers-simplify/rewrite_exists.c
+++ b/regression/cbmc/Quantifiers-simplify/rewrite_exists.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int k;
+  int k = __VERIFIER_nondet_int();
 
   __CPROVER_assume(__CPROVER_exists {
     int i;
diff --git a/regression/cbmc/Quantifiers-statement-expression3/main.c b/regression/cbmc/Quantifiers-statement-expression3/main.c
index 8a0ae9db277..0a88f2af2e7 100644
--- a/regression/cbmc/Quantifiers-statement-expression3/main.c
+++ b/regression/cbmc/Quantifiers-statement-expression3/main.c
@@ -2,7 +2,7 @@ int main()
 {
   // clang-format off
   // no side effects!
-  int j;
+  int j = __VERIFIER_nondet_int();
   int a[5] = {0 , 0, 0, 0, 0};
   assert(__CPROVER_forall { int i;  ({ ( 0 <= i && i < 4) ==> ({ int k = j; if(j < 0 || j > i) k = 1;  ( a[k] == 0); }); }) });
   // clang-format on
diff --git a/regression/cbmc/Recursion2/main.c b/regression/cbmc/Recursion2/main.c
index 1866f780a0e..d99e35206fa 100644
--- a/regression/cbmc/Recursion2/main.c
+++ b/regression/cbmc/Recursion2/main.c
@@ -5,7 +5,7 @@ void f(unsigned int counter) {
 }
 
 int main() {
-  unsigned int x;
+  unsigned int x = __VERIFIER_nondet_int();
   __CPROVER_assume(x<=10);
 
   f(x);
diff --git a/regression/cbmc/String8/main.c b/regression/cbmc/String8/main.c
index c8d0593fe25..b93f9f67bf8 100644
--- a/regression/cbmc/String8/main.c
+++ b/regression/cbmc/String8/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  _Bool branch;
+  _Bool branch = __VERIFIER_nondet__Bool();
   const char *str = 0;
 
   if(branch)
diff --git a/regression/cbmc/String_Abstraction14/pass-in-implicit.c b/regression/cbmc/String_Abstraction14/pass-in-implicit.c
index 3c2c5feb988..b77772f5a13 100644
--- a/regression/cbmc/String_Abstraction14/pass-in-implicit.c
+++ b/regression/cbmc/String_Abstraction14/pass-in-implicit.c
@@ -7,7 +7,7 @@ void use_str(char *s)
 
 int main(int argc, char *argv[])
 {
-  unsigned short len;
+  unsigned short len = __VERIFIER_nondet_short();
   char *str;
   __CPROVER_assume(len > 0);
   str = malloc(len);
diff --git a/regression/cbmc/String_Abstraction15/pass-in.c b/regression/cbmc/String_Abstraction15/pass-in.c
index 70447f784eb..7a00adb525f 100644
--- a/regression/cbmc/String_Abstraction15/pass-in.c
+++ b/regression/cbmc/String_Abstraction15/pass-in.c
@@ -7,7 +7,7 @@ void use_str(char *s)
 
 int main(int argc, char *argv[])
 {
-  unsigned short len;
+  unsigned short len = __VERIFIER_nondet_short();
   char *str;
   __CPROVER_assume(len > 0);
   str = malloc(len);
diff --git a/regression/cbmc/String_Abstraction18/strcpy.c b/regression/cbmc/String_Abstraction18/strcpy.c
index 0a3567caa9c..f862ebdc980 100644
--- a/regression/cbmc/String_Abstraction18/strcpy.c
+++ b/regression/cbmc/String_Abstraction18/strcpy.c
@@ -4,7 +4,7 @@ void *malloc(__CPROVER_size_t);
 
 char *make_str()
 {
-  unsigned short len;
+  unsigned short len = __VERIFIER_nondet_short();
   char *str;
 
   __CPROVER_assume(len > 0);
diff --git a/regression/cbmc/String_Abstraction21/strcpy2.c b/regression/cbmc/String_Abstraction21/strcpy2.c
index 03488e2c1ff..9e8daef9382 100644
--- a/regression/cbmc/String_Abstraction21/strcpy2.c
+++ b/regression/cbmc/String_Abstraction21/strcpy2.c
@@ -4,7 +4,7 @@ void *malloc(__CPROVER_size_t);
 
 char *make_str()
 {
-  unsigned short len;
+  unsigned short len = __VERIFIER_nondet_short();
   char *str;
 
   __CPROVER_assume(len > 0);
diff --git a/regression/cbmc/String_Abstraction22/main.c b/regression/cbmc/String_Abstraction22/main.c
index e7abd5c2198..785975bb796 100644
--- a/regression/cbmc/String_Abstraction22/main.c
+++ b/regression/cbmc/String_Abstraction22/main.c
@@ -3,7 +3,7 @@
 int main()
 {
   char a[100], *p;
-  _Bool x;
+  _Bool x = __VERIFIER_nondet__Bool();
 
   p = x ? strcpy(a, "asd") : strcpy(a, "abc");
   assert(p == a);
diff --git a/regression/cbmc/Struct_Initialization2/main.c b/regression/cbmc/Struct_Initialization2/main.c
index 9a04c7fd804..c970cdf5655 100644
--- a/regression/cbmc/Struct_Initialization2/main.c
+++ b/regression/cbmc/Struct_Initialization2/main.c
@@ -15,7 +15,7 @@ int main()
   assert(str_array[0].b==0);
   assert(str_array[1].b==4);
 
-  int x;
+  int x = __VERIFIER_nondet_int();
 
   // this also exists (GCC)
   str_array[0] = (struct teststr){ .a=1, .c=x };
diff --git a/regression/cbmc/Struct_Initialization5/main.c b/regression/cbmc/Struct_Initialization5/main.c
index 455c9e107c0..8fdc21d2810 100644
--- a/regression/cbmc/Struct_Initialization5/main.c
+++ b/regression/cbmc/Struct_Initialization5/main.c
@@ -8,7 +8,8 @@ struct Y {
 
 int main()
 {
-  struct X foo1;
+  struct X nondet_X(void);
+  struct X foo1 = nondet_X();
   struct Y foo2;
 
   foo2=(struct Y){ foo1 };
diff --git a/regression/cbmc/Struct_Propagation1/main.c b/regression/cbmc/Struct_Propagation1/main.c
index 56445e241b6..c2586df38df 100644
--- a/regression/cbmc/Struct_Propagation1/main.c
+++ b/regression/cbmc/Struct_Propagation1/main.c
@@ -24,7 +24,7 @@ int main()
 
   __CPROVER_assert(works.inner.x == 0, "");
 
-  _Bool b;
+  _Bool b = __VERIFIER_nondet__Bool();
   if(b)
   {
     struct S s = {42, {42}};
diff --git a/regression/cbmc/Typecast1/main.c b/regression/cbmc/Typecast1/main.c
index 75d6c7ab462..fecdf1e77cd 100644
--- a/regression/cbmc/Typecast1/main.c
+++ b/regression/cbmc/Typecast1/main.c
@@ -4,7 +4,7 @@ int main()
 {
   assert(((long long int)(unsigned long long)-1)==-1);
 
-  int a;
+  int a = __VERIFIER_nondet_int();
   __CPROVER_assume(a==-1);
   unsigned long long x = (unsigned long long) a;
   assert(x == -1);
diff --git a/regression/cbmc/Unbounded_Array1/main.c b/regression/cbmc/Unbounded_Array1/main.c
index f6855f47a2f..5ec44ddb691 100644
--- a/regression/cbmc/Unbounded_Array1/main.c
+++ b/regression/cbmc/Unbounded_Array1/main.c
@@ -1,6 +1,8 @@
 int main()
 {
-  unsigned int n, i, j, ai, aj;
+  unsigned int n = __VERIFIER_nondet_int(),
+               i = __VERIFIER_nondet_unsigned_int(),
+               j = __VERIFIER_nondet_unsigned_int(), ai, aj;
   int a[n];
 
   __CPROVER_assume(n > 10 && n < 10000000);
diff --git a/regression/cbmc/Unbounded_Array5/main.c b/regression/cbmc/Unbounded_Array5/main.c
index 783bf7cd9ba..8098b116145 100644
--- a/regression/cbmc/Unbounded_Array5/main.c
+++ b/regression/cbmc/Unbounded_Array5/main.c
@@ -2,7 +2,7 @@ int mem[__CPROVER_constant_infinity_uint];
 
 int main()
 {
-  int i, j, mem_j;
+  int i = __VERIFIER_nondet_int(), j = __VERIFIER_nondet_int(), mem_j;
 
   mem[0] = 0;
   mem[1] = 1;
diff --git a/regression/cbmc/Undefined_Shift1/main.c b/regression/cbmc/Undefined_Shift1/main.c
index 40beb2570b3..18680378cd2 100644
--- a/regression/cbmc/Undefined_Shift1/main.c
+++ b/regression/cbmc/Undefined_Shift1/main.c
@@ -1,6 +1,6 @@
 void shift_distance_too_large()
 {
-  unsigned char x;
+  unsigned char x = __VERIFIER_nondet_char();
   unsigned r = x << ((sizeof(unsigned) - 1) * 8);  // ok
   r = x << ((sizeof(unsigned) - 1) * 8 - 1);       // ok
   r = (unsigned)x << ((sizeof(unsigned) - 1) * 8); // ok
@@ -9,7 +9,7 @@ void shift_distance_too_large()
 
 void shift_distance_negative()
 {
-  int dist;
+  int dist = __VERIFIER_nondet_int();
   if(dist >= 10)
     dist = 10;
   unsigned r = 1 << dist; // distance may be negative
diff --git a/regression/cbmc/array-tests/uf-always.c b/regression/cbmc/array-tests/uf-always.c
index f53a831b2d4..e2c90c99a7b 100644
--- a/regression/cbmc/array-tests/uf-always.c
+++ b/regression/cbmc/array-tests/uf-always.c
@@ -7,7 +7,7 @@ int uninitializedGlobalArray2[2];
 int main(void)
 {
   // Variable access
-  long directUseReadLocation; // Non-det
+  long directUseReadLocation = __VERIFIER_nondet_long();
 
   long x = directUseReadLocation;
   if(0 <= directUseReadLocation && directUseReadLocation < 2)
@@ -16,7 +16,7 @@ int main(void)
   /*** Variable non-redundant update ***/
   // No obvious simplifications to writes
 
-  long nonRedundantWriteLocation;
+  long nonRedundantWriteLocation = __VERIFIER_nondet_long();
 
   if(
     0 <= nonRedundantWriteLocation && nonRedundantWriteLocation < 2 &&
diff --git a/regression/cbmc/array-tests/zero-sized.c b/regression/cbmc/array-tests/zero-sized.c
index 19a6b9083e9..6bddef81957 100644
--- a/regression/cbmc/array-tests/zero-sized.c
+++ b/regression/cbmc/array-tests/zero-sized.c
@@ -1,7 +1,7 @@
 int main()
 {
   int A[0] = {};
-  int i;
+  int i = __VERIFIER_nondet_int();
   if(A[i] == 1)
     __CPROVER_assert(0, "");
 }
diff --git a/regression/cbmc/atomic_X_fetch-1/main.c b/regression/cbmc/atomic_X_fetch-1/main.c
index 13a660c09ab..2da8b95093e 100644
--- a/regression/cbmc/atomic_X_fetch-1/main.c
+++ b/regression/cbmc/atomic_X_fetch-1/main.c
@@ -2,18 +2,18 @@
 
 void int_test()
 {
-  int *p, v, x, x_before;
+  int *p, v = __VERIFIER_nondet_int(), x = __VERIFIER_nondet_int(), x_before;
   x_before = x;
   p = &x;
 
-  int result = __atomic_add_fetch(p, v, 0);
+  int result = __atomic_add_fetch(p, v = __VERIFIER_nondet_int(), 0);
   assert(result == x);
   assert(x == x_before + v);
 }
 
 void long_test()
 {
-  long *p, v, x, x_before;
+  long *p, v = __VERIFIER_nondet_long(), x = __VERIFIER_nondet_long(), x_before;
   x_before = x;
   p = &x;
 
@@ -24,8 +24,8 @@ void long_test()
 
 void mixed_test()
 {
-  int *p, x, x_before;
-  long v;
+  int *p, x = __VERIFIER_nondet_int(), x_before;
+  long v = __VERIFIER_nondet_long();
   x_before = x;
   p = &x;
 
diff --git a/regression/cbmc/atomic_fetch_X-1/main.c b/regression/cbmc/atomic_fetch_X-1/main.c
index 28a52d5bdae..593e81cde3d 100644
--- a/regression/cbmc/atomic_fetch_X-1/main.c
+++ b/regression/cbmc/atomic_fetch_X-1/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int *p, v, x, x_before;
+  int *p, v = __VERIFIER_nondet_int(), x = __VERIFIER_nondet_int(), x_before;
   x_before = x;
   p = &x;
 
diff --git a/regression/cbmc/aws-byte-buf-regression/main.c b/regression/cbmc/aws-byte-buf-regression/main.c
index ab993262d53..46ecf252208 100644
--- a/regression/cbmc/aws-byte-buf-regression/main.c
+++ b/regression/cbmc/aws-byte-buf-regression/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  unsigned size;
+  unsigned size = __VERIFIER_nondet_unsigned();
   __CPROVER_assume(size >= sizeof(short));
   char *buf = __CPROVER_allocate(size, 0);
 
diff --git a/regression/cbmc/big-endian-array1/main.c b/regression/cbmc/big-endian-array1/main.c
index 71dc797caf0..19b27134ffb 100644
--- a/regression/cbmc/big-endian-array1/main.c
+++ b/regression/cbmc/big-endian-array1/main.c
@@ -4,7 +4,7 @@ int *array;
 
 int main()
 {
-  unsigned size;
+  unsigned size = __VERIFIER_nondet_unsigned();
   __CPROVER_assume(size==1);
 
   // produce unbounded array that does not have byte granularity
diff --git a/regression/cbmc/bounds_check1/main.c b/regression/cbmc/bounds_check1/main.c
index 7f6fb231209..6618b9a2420 100644
--- a/regression/cbmc/bounds_check1/main.c
+++ b/regression/cbmc/bounds_check1/main.c
@@ -41,7 +41,10 @@ typedef struct _eth_frame_with_control
 void stack()
 {
   eth_frame_with_control f;
-  unsigned i, i2, j, j2, k, k2, l, l2;
+  unsigned i = __VERIFIER_nondet_unsigned(), i2 = __VERIFIER_nondet_unsigned(),
+           j = __VERIFIER_nondet_unsigned(), j2 = __VERIFIER_nondet_unsigned(),
+           k = __VERIFIER_nondet_unsigned(), k2 = __VERIFIER_nondet_unsigned(),
+           l = __VERIFIER_nondet_unsigned(), l2 = __VERIFIER_nondet_unsigned();
 
   // Safe if 0 <= i < FRAME_LENGTH, viable attack over FRAME_LENGTH
   __CPROVER_assume(i < FRAME_LENGTH);
@@ -76,7 +79,10 @@ void stack()
 void heap()
 {
   eth_frame_with_control *f_heap = malloc(sizeof(eth_frame_with_control));
-  unsigned i, i2, j, j2, k, k2, l, l2;
+  unsigned i = __VERIFIER_nondet_unsigned(), i2 = __VERIFIER_nondet_unsigned(),
+           j = __VERIFIER_nondet_unsigned(), j2 = __VERIFIER_nondet_unsigned(),
+           k = __VERIFIER_nondet_unsigned(), k2 = __VERIFIER_nondet_unsigned(),
+           l = __VERIFIER_nondet_unsigned(), l2 = __VERIFIER_nondet_unsigned();
 
   // Safe if 0 <= i < FRAME_LENGTH, viable attack over FRAME_LENGTH
   __CPROVER_assume(i < FRAME_LENGTH);
diff --git a/regression/cbmc/byte_update11/main.c b/regression/cbmc/byte_update11/main.c
index 02bcf96660a..6d8b85b6778 100644
--- a/regression/cbmc/byte_update11/main.c
+++ b/regression/cbmc/byte_update11/main.c
@@ -5,7 +5,7 @@ struct S
 
 int main()
 {
-  int x;
+  int x = __VERIFIER_nondet_int();
   __CPROVER_assume(x >= 0);
   __CPROVER_assume(x % sizeof(int) == 0);
   struct S A[x];
diff --git a/regression/cbmc/byte_update12/main.c b/regression/cbmc/byte_update12/main.c
index 135136dbd61..8831919cc7e 100644
--- a/regression/cbmc/byte_update12/main.c
+++ b/regression/cbmc/byte_update12/main.c
@@ -8,7 +8,7 @@ struct S
 
 int main()
 {
-  unsigned x;
+  unsigned x = __VERIFIER_nondet_unsigned();
   char A[x];
   __CPROVER_assume(x == sizeof(int));
   A[0] = 42;
diff --git a/regression/cbmc/byte_update15/main.c b/regression/cbmc/byte_update15/main.c
index df8eb3d9968..2c13e7dfa05 100644
--- a/regression/cbmc/byte_update15/main.c
+++ b/regression/cbmc/byte_update15/main.c
@@ -3,7 +3,7 @@
 
 int main(void)
 {
-  int src[8], dst[8], delta;
+  int src[8], dst[8], delta = __VERIFIER_nondet_int();
   if(delta == 3 || delta == 4)
   {
     memcpy(dst, src, sizeof(int) * delta);
diff --git a/regression/cbmc/byte_update16/main.c b/regression/cbmc/byte_update16/main.c
index e68541f1eae..6f9f0ea195c 100644
--- a/regression/cbmc/byte_update16/main.c
+++ b/regression/cbmc/byte_update16/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  unsigned len;
+  unsigned len = __VERIFIER_nondet_unsigned();
   unsigned A[len];
   if(len > 1 || len == 0 || sizeof(unsigned) != 4)
     return 0;
diff --git a/regression/cbmc/byte_update17/main.c b/regression/cbmc/byte_update17/main.c
index 5cad8ee6fee..61821a36e16 100644
--- a/regression/cbmc/byte_update17/main.c
+++ b/regression/cbmc/byte_update17/main.c
@@ -9,7 +9,7 @@ union U
 
 int main()
 {
-  unsigned char size;
+  unsigned char size = __VERIFIER_nondet_char();
   __CPROVER_assume(size > 1);
   __CPROVER_assume(size < 5);
   __CPROVER_assume(size % 4 == 0);
diff --git a/regression/cbmc/byte_update18/main.c b/regression/cbmc/byte_update18/main.c
index a172611ae9e..3473d0cf847 100644
--- a/regression/cbmc/byte_update18/main.c
+++ b/regression/cbmc/byte_update18/main.c
@@ -13,7 +13,7 @@ struct O
 int main()
 {
   struct O t = {{{{0}, 2}, {{42}, 2}}, 2};
-  unsigned n;
+  unsigned n = __VERIFIER_nondet_unsigned();
   __CPROVER_assume(n < 2);
   __CPROVER_assume(n > 0);
   char src_n[n];
diff --git a/regression/cbmc/clang_builtins/bitreverse.c b/regression/cbmc/clang_builtins/bitreverse.c
index 2a708015fa5..d4c788f56ea 100644
--- a/regression/cbmc/clang_builtins/bitreverse.c
+++ b/regression/cbmc/clang_builtins/bitreverse.c
@@ -29,28 +29,28 @@ unsigned long long __builtin_bitreverse64(unsigned long long);
 
 void check_8(void)
 {
-  uint8_t op;
+  uint8_t op = __VERIFIER_nondet_uint8_t();
   assert(__builtin_bitreverse8(op) == test_bit_reverse8(op));
   assert(__builtin_bitreverse8(1) == 0x80);
 }
 
 void check_16(void)
 {
-  uint16_t op;
+  uint16_t op = __VERIFIER_nondet_uint16_t();
   assert(__builtin_bitreverse16(op) == test_bit_reverse16(op));
   assert(__builtin_bitreverse16(1) == 0x8000);
 }
 
 void check_32(void)
 {
-  uint32_t op;
+  uint32_t op = __VERIFIER_nondet_uint32_t();
   assert(__builtin_bitreverse32(op) == test_bit_reverse32(op));
   assert(__builtin_bitreverse32(1) == 0x80000000);
 }
 
 void check_64(void)
 {
-  uint64_t op;
+  uint64_t op = __VERIFIER_nondet_uint64_t();
   assert(__builtin_bitreverse64(op) == test_bit_reverse64(op));
   assert(__builtin_bitreverse64(1) == 0x8000000000000000ULL);
 }
diff --git a/regression/cbmc/clang_builtins/rotate.c b/regression/cbmc/clang_builtins/rotate.c
index 0f4df6cb213..4ccf18666b3 100644
--- a/regression/cbmc/clang_builtins/rotate.c
+++ b/regression/cbmc/clang_builtins/rotate.c
@@ -24,7 +24,7 @@ __builtin_rotateright64(unsigned long long, unsigned long long);
 
 void check_left8(void)
 {
-  uint8_t op;
+  uint8_t op = __VERIFIER_nondet_uint8_t();
   assert(__builtin_rotateleft8(op, 1) == rol(uint8_t, op, 1));
   assert(__builtin_rotateleft8(op, 2) == rol(uint8_t, op, 2));
   assert(__builtin_rotateleft8(op, 3) == rol(uint8_t, op, 3));
@@ -33,7 +33,7 @@ void check_left8(void)
 
 void check_left16(void)
 {
-  uint16_t op;
+  uint16_t op = __VERIFIER_nondet_uint16_t();
   assert(__builtin_rotateleft16(op, 1) == rol(uint16_t, op, 1));
   assert(__builtin_rotateleft16(op, 2) == rol(uint16_t, op, 2));
   assert(__builtin_rotateleft16(op, 3) == rol(uint16_t, op, 3));
@@ -42,7 +42,7 @@ void check_left16(void)
 
 void check_left32(void)
 {
-  uint32_t op;
+  uint32_t op = __VERIFIER_nondet_uint32_t();
   assert(__builtin_rotateleft32(op, 1) == rol(uint32_t, op, 1));
   assert(__builtin_rotateleft32(op, 2) == rol(uint32_t, op, 2));
   assert(__builtin_rotateleft32(op, 3) == rol(uint32_t, op, 3));
@@ -51,7 +51,7 @@ void check_left32(void)
 
 void check_left64(void)
 {
-  uint64_t op;
+  uint64_t op = __VERIFIER_nondet_uint64_t();
   assert(__builtin_rotateleft64(op, 1) == rol(uint64_t, op, 1));
   assert(__builtin_rotateleft64(op, 2) == rol(uint64_t, op, 2));
   assert(__builtin_rotateleft64(op, 3) == rol(uint64_t, op, 3));
@@ -60,7 +60,7 @@ void check_left64(void)
 
 void check_right8(void)
 {
-  uint8_t op;
+  uint8_t op = __VERIFIER_nondet_uint8_t();
   assert(__builtin_rotateright8(op, 1) == ror(uint8_t, op, 1));
   assert(__builtin_rotateright8(op, 2) == ror(uint8_t, op, 2));
   assert(__builtin_rotateright8(op, 3) == ror(uint8_t, op, 3));
@@ -69,7 +69,7 @@ void check_right8(void)
 
 void check_right16(void)
 {
-  uint16_t op;
+  uint16_t op = __VERIFIER_nondet_uint16_t();
   assert(__builtin_rotateright16(op, 1) == ror(uint16_t, op, 1));
   assert(__builtin_rotateright16(op, 2) == ror(uint16_t, op, 2));
   assert(__builtin_rotateright16(op, 3) == ror(uint16_t, op, 3));
@@ -78,7 +78,7 @@ void check_right16(void)
 
 void check_right32(void)
 {
-  uint32_t op;
+  uint32_t op = __VERIFIER_nondet_uint32_t();
   assert(__builtin_rotateright32(op, 1) == ror(uint32_t, op, 1));
   assert(__builtin_rotateright32(op, 2) == ror(uint32_t, op, 2));
   assert(__builtin_rotateright32(op, 3) == ror(uint32_t, op, 3));
@@ -87,7 +87,7 @@ void check_right32(void)
 
 void check_right64(void)
 {
-  uint64_t op;
+  uint64_t op = __VERIFIER_nondet_uint64_t();
   assert(__builtin_rotateright64(op, 1) == ror(uint64_t, op, 1));
   assert(__builtin_rotateright64(op, 2) == ror(uint64_t, op, 2));
   assert(__builtin_rotateright64(op, 3) == ror(uint64_t, op, 3));
diff --git a/regression/cbmc/condition-propagation-4/test.c b/regression/cbmc/condition-propagation-4/test.c
index 945fc8c3357..44823a7d3f9 100644
--- a/regression/cbmc/condition-propagation-4/test.c
+++ b/regression/cbmc/condition-propagation-4/test.c
@@ -1,6 +1,6 @@
 int main(int argc, char **argv)
 {
-  int unknown;
+  int unknown = __VERIFIER_nondet_int();
 
   if(argc != 1)
   {
diff --git a/regression/cbmc/divide-by-one-simplify/main.c b/regression/cbmc/divide-by-one-simplify/main.c
index dfe632ba932..5a6c4725ca1 100644
--- a/regression/cbmc/divide-by-one-simplify/main.c
+++ b/regression/cbmc/divide-by-one-simplify/main.c
@@ -1,7 +1,7 @@
 #include <assert.h>
 
 int main (void) {
-  float f;
+  float f = __VERIFIER_nondet_float();
   float g;
   int i;
 
diff --git a/regression/cbmc/dynamic_size1/stack_object.c b/regression/cbmc/dynamic_size1/stack_object.c
index b3c7e758fed..85371acd727 100644
--- a/regression/cbmc/dynamic_size1/stack_object.c
+++ b/regression/cbmc/dynamic_size1/stack_object.c
@@ -14,7 +14,7 @@ void func(struct S *s)
 
 int main()
 {
-  __CPROVER_size_t buffer_size;
+  __CPROVER_size_t buffer_size = __VERIFIER_nondet___CPROVER_size_t();
   __CPROVER_assume(buffer_size >= 100);
   char buffer[buffer_size];
   struct S s;
diff --git a/regression/cbmc/dynamic_sizeof1/main.c b/regression/cbmc/dynamic_sizeof1/main.c
index dee1908ada7..5d33b19d555 100644
--- a/regression/cbmc/dynamic_sizeof1/main.c
+++ b/regression/cbmc/dynamic_sizeof1/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  unsigned x;
+  unsigned x = __VERIFIER_nondet_unsigned();
 
   if(x>=0 && x<=1000)
   {
diff --git a/regression/cbmc/enum9/main.c b/regression/cbmc/enum9/main.c
index 2b9a61c3698..71b954c49e2 100644
--- a/regression/cbmc/enum9/main.c
+++ b/regression/cbmc/enum9/main.c
@@ -13,13 +13,14 @@ struct B
 
 int main()
 {
-  unsigned __int128 int x;
+  unsigned __int128 int x = __VERIFIER_nondet_int();
   __CPROVER_assume(x < (~(unsigned __int128)0) - 4);
 
-  enum E e;
+  enum E e = __VERIFIER_nondet_int();
   __CPROVER_assume(__CPROVER_enum_is_in_range(e));
   __CPROVER_assert(x + e > x, "long long plus enum");
 
-  struct B b;
+  struct B nondet_B(void);
+  struct B b = nondet_B();
   __CPROVER_assert(x + b.b >= x, "long long plus bitfield");
 }
diff --git a/regression/cbmc/equality_through_array1/main.c b/regression/cbmc/equality_through_array1/main.c
index d6e7b1ba972..d1ab9d2327d 100644
--- a/regression/cbmc/equality_through_array1/main.c
+++ b/regression/cbmc/equality_through_array1/main.c
@@ -7,8 +7,8 @@ void main ()
   a[2] = 2;
   a[3] = 3;
 
-  int x;
-  int y;
+  int x = __VERIFIER_nondet_int();
+  int y = __VERIFIER_nondet_int();
 
   __CPROVER_assume(0 <= x && x < 4);
   __CPROVER_assume(0 <= y && y < 4);
diff --git a/regression/cbmc/equality_through_array2/main.c b/regression/cbmc/equality_through_array2/main.c
index 1bbe4f2340f..a752337cd9c 100644
--- a/regression/cbmc/equality_through_array2/main.c
+++ b/regression/cbmc/equality_through_array2/main.c
@@ -8,8 +8,8 @@ void main ()
     a[i] = i;
   }
 
-  int x;
-  int y;
+  int x = __VERIFIER_nondet_int();
+  int y = __VERIFIER_nondet_int();
 
   __CPROVER_assume(0 <= x && x < LIMIT);
   __CPROVER_assume(0 <= y && y < LIMIT);
diff --git a/regression/cbmc/equality_through_array3/main.c b/regression/cbmc/equality_through_array3/main.c
index 9e94a5eba95..73b57e87850 100644
--- a/regression/cbmc/equality_through_array3/main.c
+++ b/regression/cbmc/equality_through_array3/main.c
@@ -15,8 +15,8 @@ void main ()
 
   fill_array(a,LIMIT);
 
-  int x;
-  int y;
+  int x = __VERIFIER_nondet_int();
+  int y = __VERIFIER_nondet_int();
 
   __CPROVER_assume(0 <= x && x < LIMIT);
   __CPROVER_assume(0 <= y && y < LIMIT);
diff --git a/regression/cbmc/equality_through_array4/main.c b/regression/cbmc/equality_through_array4/main.c
index 06fe628b50a..0aae5c718d3 100644
--- a/regression/cbmc/equality_through_array4/main.c
+++ b/regression/cbmc/equality_through_array4/main.c
@@ -15,7 +15,7 @@ int pass_through_array (int x)
 }
 
 int main (void) {
-  int x;
+  int x = __VERIFIER_nondet_int();
 
   assert(x == pass_through_array(x));
 
diff --git a/regression/cbmc/equality_through_array5/main.c b/regression/cbmc/equality_through_array5/main.c
index 41102922960..c4fcc161aae 100644
--- a/regression/cbmc/equality_through_array5/main.c
+++ b/regression/cbmc/equality_through_array5/main.c
@@ -16,7 +16,7 @@ int pass_through_array (int x)
 }
 
 int main (void) {
-  int x;
+  int x = __VERIFIER_nondet_int();
 
   assert(x == pass_through_array(x));
 
diff --git a/regression/cbmc/equality_through_array6/main.c b/regression/cbmc/equality_through_array6/main.c
index 82fd4cfa2bd..4b9bb4c6369 100644
--- a/regression/cbmc/equality_through_array6/main.c
+++ b/regression/cbmc/equality_through_array6/main.c
@@ -16,7 +16,7 @@ int pass_through_array (int x)
 }
 
 int main (void) {
-  int x;
+  int x = __VERIFIER_nondet_int();
 
   assert(x == pass_through_array(x));
 
diff --git a/regression/cbmc/equality_through_array_of_struct1/main.c b/regression/cbmc/equality_through_array_of_struct1/main.c
index e05a4f2fee9..948dc85ea3c 100644
--- a/regression/cbmc/equality_through_array_of_struct1/main.c
+++ b/regression/cbmc/equality_through_array_of_struct1/main.c
@@ -13,7 +13,7 @@ struct str a[SIZE];
 
 int main (void)
 {
-  int q;
+  int q = __VERIFIER_nondet_int();
 
   a[0].x = q;
   a[1].y = a[0].x;
diff --git a/regression/cbmc/equality_through_array_of_struct2/main.c b/regression/cbmc/equality_through_array_of_struct2/main.c
index 49605bf908f..69fb75952eb 100644
--- a/regression/cbmc/equality_through_array_of_struct2/main.c
+++ b/regression/cbmc/equality_through_array_of_struct2/main.c
@@ -13,7 +13,7 @@ struct str a[SIZE];
 
 int main (void)
 {
-  int q;
+  int q = __VERIFIER_nondet_int();
 
   for (int i = 0; i < SIZE; ++i)
   {
diff --git a/regression/cbmc/equality_through_array_of_struct3/main.c b/regression/cbmc/equality_through_array_of_struct3/main.c
index fd81ad150e8..f4a5fb025de 100644
--- a/regression/cbmc/equality_through_array_of_struct3/main.c
+++ b/regression/cbmc/equality_through_array_of_struct3/main.c
@@ -23,7 +23,7 @@ void pass_through_array_of_struct (int q)
 
 int main (void)
 {
-  int q;
+  int q = __VERIFIER_nondet_int();
 
   pass_through_array_of_struct(q);
 
diff --git a/regression/cbmc/equality_through_array_of_struct4/main.c b/regression/cbmc/equality_through_array_of_struct4/main.c
index 9769b5d5cf9..cc792a4e27e 100644
--- a/regression/cbmc/equality_through_array_of_struct4/main.c
+++ b/regression/cbmc/equality_through_array_of_struct4/main.c
@@ -30,7 +30,7 @@ int pass_through_array_of_struct (int q)
 
 int main (void)
 {
-  int q;
+  int q = __VERIFIER_nondet_int();
 
   assert(q == pass_through_array_of_struct(q));
 
diff --git a/regression/cbmc/equality_through_struct1/main.c b/regression/cbmc/equality_through_struct1/main.c
index 5b78b7af31d..41cefef6d2c 100644
--- a/regression/cbmc/equality_through_struct1/main.c
+++ b/regression/cbmc/equality_through_struct1/main.c
@@ -9,7 +9,7 @@ struct str
 
 int main (void)
 {
-  int q;
+  int q = __VERIFIER_nondet_int();
   struct str s;
 
   s.x = q;
diff --git a/regression/cbmc/equality_through_struct2/main.c b/regression/cbmc/equality_through_struct2/main.c
index 11d8f67037a..46c392d13f5 100644
--- a/regression/cbmc/equality_through_struct2/main.c
+++ b/regression/cbmc/equality_through_struct2/main.c
@@ -20,7 +20,7 @@ int pass_through_struct (int q)
 
 int main (void)
 {
-  int q;
+  int q = __VERIFIER_nondet_int();
 
   assert(q == pass_through_struct(q));
 
diff --git a/regression/cbmc/equality_through_struct3/main.c b/regression/cbmc/equality_through_struct3/main.c
index 749f1e6f4a9..bac176623fc 100644
--- a/regression/cbmc/equality_through_struct3/main.c
+++ b/regression/cbmc/equality_through_struct3/main.c
@@ -20,7 +20,7 @@ struct str pass_through_struct (int q)
 
 int main (void)
 {
-  int q;
+  int q = __VERIFIER_nondet_int();
 
   struct str s = pass_through_struct(q);
 
diff --git a/regression/cbmc/equality_through_struct4/main.c b/regression/cbmc/equality_through_struct4/main.c
index 966221229ac..19067371814 100644
--- a/regression/cbmc/equality_through_struct4/main.c
+++ b/regression/cbmc/equality_through_struct4/main.c
@@ -18,7 +18,7 @@ void pass_through_struct (struct str *s, int q)
 
 int main (void)
 {
-  int q;
+  int q = __VERIFIER_nondet_int();
 
   struct str s;
 
diff --git a/regression/cbmc/equality_through_struct_containing_arrays1/main.c b/regression/cbmc/equality_through_struct_containing_arrays1/main.c
index 4b88e22f3b9..0f22438dc6f 100644
--- a/regression/cbmc/equality_through_struct_containing_arrays1/main.c
+++ b/regression/cbmc/equality_through_struct_containing_arrays1/main.c
@@ -33,7 +33,7 @@ void pass_through_struct_containing_arrays (int q)
 
 int main (void)
 {
-  int q;
+  int q = __VERIFIER_nondet_int();
 
   pass_through_struct_containing_arrays(q);
 
diff --git a/regression/cbmc/equality_through_struct_containing_arrays2/main.c b/regression/cbmc/equality_through_struct_containing_arrays2/main.c
index a10f7cf2ec4..fcfc8f31e12 100644
--- a/regression/cbmc/equality_through_struct_containing_arrays2/main.c
+++ b/regression/cbmc/equality_through_struct_containing_arrays2/main.c
@@ -33,7 +33,7 @@ void pass_through_struct_containing_arrays (int q, int j)
 
 int main (void)
 {
-  int q;
+  int q = __VERIFIER_nondet_int();
 
   s[1].z = 0;
 
diff --git a/regression/cbmc/equality_through_union1/main.c b/regression/cbmc/equality_through_union1/main.c
index 39d7ae9ed28..f2016787adc 100644
--- a/regression/cbmc/equality_through_union1/main.c
+++ b/regression/cbmc/equality_through_union1/main.c
@@ -10,21 +10,21 @@ union u
 
 union u pass_through_union (int32_t q)
 {
-  union u un;
+   union u un;
 
-  un.z[0] = 0;
-  un.y = q;
+   un.z[0] = 0;
+   un.y = q;
 
-  return un;
+   return un;
 }
 
 int main (void)
 {
-  int32_t q;
+   int32_t q = __VERIFIER_nondet_int32_t();
 
-  union u un = pass_through_union(q);
+   union u un = pass_through_union(q);
 
-  assert(q == un.y);
+   assert(q == un.y);
 
-  return 1;
+   return 1;
 }
diff --git a/regression/cbmc/equality_through_union2/main.c b/regression/cbmc/equality_through_union2/main.c
index 70a6acd8cdb..478ec8ce3ef 100644
--- a/regression/cbmc/equality_through_union2/main.c
+++ b/regression/cbmc/equality_through_union2/main.c
@@ -10,23 +10,23 @@ union u
 
 union u pass_through_union (int32_t q)
 {
-  union u un;
+   union u un;
 
-  un.z[0] = 0;
-  un.y = q;
+   un.z[0] = 0;
+   un.y = q;
 
-  return un;
+   return un;
 }
 
 int main (void)
 {
-  int32_t q;
+   int32_t q = __VERIFIER_nondet_int32_t();
 
-  __CPROVER_assume(q > 0);
+   __CPROVER_assume(q > 0);
 
-  union u un = pass_through_union(q);
+   union u un = pass_through_union(q);
 
-  assert(q == un.x);
+   assert(q == un.x);
 
-  return 1;
+   return 1;
 }
diff --git a/regression/cbmc/equality_through_union3/main.c b/regression/cbmc/equality_through_union3/main.c
index ccc03df0596..a8d4590d3fd 100644
--- a/regression/cbmc/equality_through_union3/main.c
+++ b/regression/cbmc/equality_through_union3/main.c
@@ -10,26 +10,26 @@ union u
 
 union u pass_through_union (uint32_t q)
 {
-  union u un;
+   union u un;
 
-  un.z[0] = 0x0;
-  un.y = q;
-  un.z[3] = 0x0;
-  un.z[0] = 0x0;
+   un.z[0] = 0x0;
+   un.y = q;
+   un.z[3] = 0x0;
+   un.z[0] = 0x0;
 
-  return un;
+   return un;
 }
 
 int main (void)
 {
-  uint32_t q;
+   uint32_t q = __VERIFIER_nondet_uint32_t();
 
-  __CPROVER_assume((q & q - 1) == 0);
-  __CPROVER_assume(256 <= q && q <= (1 << 23));
+   __CPROVER_assume((q & q - 1) == 0);
+   __CPROVER_assume(256 <= q && q <= (1 << 23));
 
-  union u un = pass_through_union(q);
+   union u un = pass_through_union(q);
 
-  assert(q == un.y);
+   assert(q == un.y);
 
-  return 1;
+   return 1;
 }
diff --git a/regression/cbmc/exit1/main.c b/regression/cbmc/exit1/main.c
index c403cc204f0..f7b935496a6 100644
--- a/regression/cbmc/exit1/main.c
+++ b/regression/cbmc/exit1/main.c
@@ -1,7 +1,7 @@
 void exit(int status);
 
 int main() {
-  int x;
+  int x = __VERIFIER_nondet_int();
 
   if(x==10)
     exit(1);
diff --git a/regression/cbmc/field-sensitivity15/main.c b/regression/cbmc/field-sensitivity15/main.c
index bbe22ad46ca..4e463610eb9 100644
--- a/regression/cbmc/field-sensitivity15/main.c
+++ b/regression/cbmc/field-sensitivity15/main.c
@@ -18,7 +18,7 @@ union _14237415465709481864_union
 
 void main(void)
 {
-  unsigned int x; // nondet
+  unsigned int x = __VERIFIER_nondet_int(); // nondet
 
   // the following is crucial (else pn trivially simplifies to 0)
   unsigned int var_7 = x;
diff --git a/regression/cbmc/field-sensitivity16/main.c b/regression/cbmc/field-sensitivity16/main.c
index bfec1b50970..4bec39e65f4 100644
--- a/regression/cbmc/field-sensitivity16/main.c
+++ b/regression/cbmc/field-sensitivity16/main.c
@@ -33,7 +33,7 @@ union _14237415465709481864_union
 
 void main(void)
 {
-  unsigned int x; // nondet
+  unsigned int x = __VERIFIER_nondet_int(); // nondet
 
   // the following is crucial (else pn trivially simplifies to 0)
   unsigned int var_7 = x;
diff --git a/regression/cbmc/gcc_switch_case_range1/main.c b/regression/cbmc/gcc_switch_case_range1/main.c
index de9e12b0fd2..0c5e576cbdf 100644
--- a/regression/cbmc/gcc_switch_case_range1/main.c
+++ b/regression/cbmc/gcc_switch_case_range1/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int x;
+  int x = __VERIFIER_nondet_int();
   switch(x)
   {
   case 0:
diff --git a/regression/cbmc/gcc_switch_case_range2/main.c b/regression/cbmc/gcc_switch_case_range2/main.c
index 6858a9e8c3a..7fa16e7dd98 100644
--- a/regression/cbmc/gcc_switch_case_range2/main.c
+++ b/regression/cbmc/gcc_switch_case_range2/main.c
@@ -8,7 +8,7 @@ typedef enum
 
 int main()
 {
-  unsigned x;
+  unsigned x = __VERIFIER_nondet_unsigned();
   switch(x)
   {
   case VALUE_1:
diff --git a/regression/cbmc/gcc_vector1/main.c b/regression/cbmc/gcc_vector1/main.c
index 6c454459d66..831f41ee7cf 100644
--- a/regression/cbmc/gcc_vector1/main.c
+++ b/regression/cbmc/gcc_vector1/main.c
@@ -16,7 +16,8 @@ int main()
   assert(sizeof(int)==4);
   assert(sizeof(v4si)==16);
 
-  vector_u x, y, z;
+  vector_u nondet_vu(void);
+  vector_u x = nondet_vu(), y = nondet_vu(), z;
 
   // vector operator vector
   z.v=x.v+y.v;
diff --git a/regression/cbmc/goto1/main.c b/regression/cbmc/goto1/main.c
index 1eaf79a78d0..fc9f56a17da 100644
--- a/regression/cbmc/goto1/main.c
+++ b/regression/cbmc/goto1/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int i, j;
+  int i = __VERIFIER_nondet_int(), j = __VERIFIER_nondet_int();
 
   if(i)
     goto l;
diff --git a/regression/cbmc/goto2/main.c b/regression/cbmc/goto2/main.c
index 26219e65fe3..dacdf2b1592 100644
--- a/regression/cbmc/goto2/main.c
+++ b/regression/cbmc/goto2/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int i, j;
+  int i, j = __VERIFIER_nondet_int();
 
   i=1;
 
diff --git a/regression/cbmc/guard1/main.c b/regression/cbmc/guard1/main.c
index d84f80cd009..968fda75070 100644
--- a/regression/cbmc/guard1/main.c
+++ b/regression/cbmc/guard1/main.c
@@ -1,15 +1,16 @@
 int main()
 {
-int i;
-int j;
-while(i) j = j + 1;
+  int i = __VERIFIER_nondet_int();
+  int j = __VERIFIER_nondet_int();
+  while(i)
+    j = j + 1;
 }
 
 /*
 #include <assert.h>
 
 int main (void) {
-	int i;
+	int i = __VERIFIER_nondet_int();
 
 	while (1) {
 		i++;
diff --git a/regression/cbmc/havoc_object1/main.c b/regression/cbmc/havoc_object1/main.c
index dc632dd65ad..06e35a53a89 100644
--- a/regression/cbmc/havoc_object1/main.c
+++ b/regression/cbmc/havoc_object1/main.c
@@ -16,7 +16,7 @@ int main()
   __CPROVER_assert(some_struct.j==2, "struct j"); // should fail
 
   // now conditional
-  _Bool c;
+  _Bool c = __VERIFIER_nondet__Bool();
   int *p=c?&i:&some_struct.i;
   i=20;
   some_struct.i=30;
diff --git a/regression/cbmc/if1/main.c b/regression/cbmc/if1/main.c
index 9a0b65d37f6..911a2519e2b 100644
--- a/regression/cbmc/if1/main.c
+++ b/regression/cbmc/if1/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int i, j;
+  int i, j = __VERIFIER_nondet_int();
 
   i = 1;
 
diff --git a/regression/cbmc/if4/main.c b/regression/cbmc/if4/main.c
index e109c21dbd5..6241571d7fe 100644
--- a/regression/cbmc/if4/main.c
+++ b/regression/cbmc/if4/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int x;
+  int x = __VERIFIER_nondet_int();
 
   __CPROVER_assume(x==1);
 
diff --git a/regression/cbmc/inequality-with-constant-normalisation/main.c b/regression/cbmc/inequality-with-constant-normalisation/main.c
index 26de92f9e64..fdfe40b9b14 100644
--- a/regression/cbmc/inequality-with-constant-normalisation/main.c
+++ b/regression/cbmc/inequality-with-constant-normalisation/main.c
@@ -3,7 +3,7 @@
 #include <assert.h>
 
 int main (void) {
-  int x;
+  int x = __VERIFIER_nondet_int();
 
   while ((x >= 10) && (x < 10)) {}
   while ((x >= 10) && (x <= 9)) {}
diff --git a/regression/cbmc/inequality-with-constant-normalisation1/main.c b/regression/cbmc/inequality-with-constant-normalisation1/main.c
index 0d0cfddf352..133f8a624ec 100644
--- a/regression/cbmc/inequality-with-constant-normalisation1/main.c
+++ b/regression/cbmc/inequality-with-constant-normalisation1/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  _Bool b1, b2;
+  _Bool b1 = __VERIFIER_nondet__Bool(), b2 = __VERIFIER_nondet__Bool();
 
   int nc = (b1 ? 1 : 2) == (b2 ? 1 : 2);
   assert(b1 != b2 || nc != 0);
diff --git a/regression/cbmc/lhs-pointer-aliases-constant/test.c b/regression/cbmc/lhs-pointer-aliases-constant/test.c
index 82bb49bf4c7..4cd412a9796 100644
--- a/regression/cbmc/lhs-pointer-aliases-constant/test.c
+++ b/regression/cbmc/lhs-pointer-aliases-constant/test.c
@@ -4,7 +4,7 @@ int main()
 {
   int x;
   const char *c = "Hello world";
-  _Bool dummy;
+  _Bool dummy = __VERIFIER_nondet__Bool();
   __CPROVER_assume(dummy);
 
   int *p = (dummy ? &x : (int *)c);
diff --git a/regression/cbmc/little-endian-array1/main.c b/regression/cbmc/little-endian-array1/main.c
index 5919db3e3c1..70827a6ca5a 100644
--- a/regression/cbmc/little-endian-array1/main.c
+++ b/regression/cbmc/little-endian-array1/main.c
@@ -4,7 +4,7 @@ int *array;
 
 int main()
 {
-  unsigned size;
+  unsigned size = __VERIFIER_nondet_unsigned();
   __CPROVER_assume(size==1);
 
   // produce unbounded array that does not have byte granularity
diff --git a/regression/cbmc/no-propagation/main.c b/regression/cbmc/no-propagation/main.c
index d6134ea6583..5b0bb450623 100644
--- a/regression/cbmc/no-propagation/main.c
+++ b/regression/cbmc/no-propagation/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int x;
+  int x = __VERIFIER_nondet_int();
   if(x == 1)
     __CPROVER_assert(x == 1, "");
 }
diff --git a/regression/cbmc/null7/main.c b/regression/cbmc/null7/main.c
index da3b1d30c2b..9ee585f5ccb 100644
--- a/regression/cbmc/null7/main.c
+++ b/regression/cbmc/null7/main.c
@@ -16,7 +16,7 @@ int main()
 
   if(s_is_set)
   {
-    unsigned len;
+    unsigned len = __VERIFIER_nondet_unsigned();
     __CPROVER_assume(len < 3);
     s += len;
   }
diff --git a/regression/cbmc/overflow/leftshift_overflow.c b/regression/cbmc/overflow/leftshift_overflow.c
index 6c6ff862941..ea2afa7913b 100644
--- a/regression/cbmc/overflow/leftshift_overflow.c
+++ b/regression/cbmc/overflow/leftshift_overflow.c
@@ -48,7 +48,7 @@ void leftshift_overflow7(unsigned char x)
 void leftshift_overflow8(unsigned char x)
 {
   // overflow in an expression where operand and distance types are different
-  uint32_t u32;
+  uint32_t u32 = __VERIFIER_nondet_uint32_t();
   int64_t i64 = ((int64_t)u32) << 32;
 }
 
diff --git a/regression/cbmc/overflow/signed_multiplication1.c b/regression/cbmc/overflow/signed_multiplication1.c
index a04ad8ac09d..1034241efd7 100644
--- a/regression/cbmc/overflow/signed_multiplication1.c
+++ b/regression/cbmc/overflow/signed_multiplication1.c
@@ -2,7 +2,7 @@
 
 void main()
 {
-  int x, y, _x, _y;
+  int x, y, _x = __VERIFIER_nondet_int(), _y = __VERIFIER_nondet_int();
 
   x = _x;
   y = _y;
diff --git a/regression/cbmc/overflow/signed_subtraction1.c b/regression/cbmc/overflow/signed_subtraction1.c
index 4e9faf2af7f..8ac3133f219 100644
--- a/regression/cbmc/overflow/signed_subtraction1.c
+++ b/regression/cbmc/overflow/signed_subtraction1.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int a, b, neg;
+  int a = __VERIFIER_nondet_int(), b, neg = __VERIFIER_nondet_int();
 
   // this should not overflow, even not for a=INT_MIN
   b = a - a;
diff --git a/regression/cbmc/pointer-predicates/at_bounds1.c b/regression/cbmc/pointer-predicates/at_bounds1.c
index e28114b0480..742543867ae 100644
--- a/regression/cbmc/pointer-predicates/at_bounds1.c
+++ b/regression/cbmc/pointer-predicates/at_bounds1.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  size_t s;
+  size_t s = __VERIFIER_nondet_size_t();
   char *p = malloc(s);
   // at __CPROVER_max_malloc_size p + s would overflow; all larger values of s
   // make malloc return NULL when using --malloc-fail-null
diff --git a/regression/cbmc/pragma_cprover1/main.c b/regression/cbmc/pragma_cprover1/main.c
index c59252f5ca6..a877edd80f2 100644
--- a/regression/cbmc/pragma_cprover1/main.c
+++ b/regression/cbmc/pragma_cprover1/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int x;
+  int x = __VERIFIER_nondet_int();
   int y[1];
 
 #pragma CPROVER check push
diff --git a/regression/cbmc/pragma_cprover2/main.c b/regression/cbmc/pragma_cprover2/main.c
index 1a10fb48fa0..2a9d1204a24 100644
--- a/regression/cbmc/pragma_cprover2/main.c
+++ b/regression/cbmc/pragma_cprover2/main.c
@@ -5,7 +5,7 @@ int foo(int x)
 
 int main()
 {
-  int m, n;
+  int m, n = __VERIFIER_nondet_int();
 
 #pragma CPROVER check push
 #pragma CPROVER check disable "signed-overflow"
diff --git a/regression/cbmc/pragma_cprover_enable1/main.c b/regression/cbmc/pragma_cprover_enable1/main.c
index 473534f3f11..9203075fdbf 100644
--- a/regression/cbmc/pragma_cprover_enable1/main.c
+++ b/regression/cbmc/pragma_cprover_enable1/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int x;
+  int x = __VERIFIER_nondet_int();
   int y[1];
 
 #pragma CPROVER check push
diff --git a/regression/cbmc/pragma_cprover_enable2/main.c b/regression/cbmc/pragma_cprover_enable2/main.c
index 6c59fe18282..2609cc26709 100644
--- a/regression/cbmc/pragma_cprover_enable2/main.c
+++ b/regression/cbmc/pragma_cprover_enable2/main.c
@@ -5,7 +5,7 @@ int foo(int x)
 
 int main()
 {
-  int m, n;
+  int m, n = __VERIFIER_nondet_int();
 
 #pragma CPROVER check push
 #pragma CPROVER check enable "signed-overflow"
diff --git a/regression/cbmc/r_w_ok1/main.c b/regression/cbmc/r_w_ok1/main.c
index 0a24178df9c..2ece5ccfb65 100644
--- a/regression/cbmc/r_w_ok1/main.c
+++ b/regression/cbmc/r_w_ok1/main.c
@@ -15,7 +15,7 @@ int main()
   assert(__CPROVER_r_ok(p, sizeof(int)));
   assert(__CPROVER_w_ok(p, sizeof(int)));
 
-  size_t n;
+  size_t n = __VERIFIER_nondet_size_t();
   char *arbitrary_size = malloc(n);
 
   assert(__CPROVER_r_ok(arbitrary_size, n));
diff --git a/regression/cbmc/r_w_ok7/main.c b/regression/cbmc/r_w_ok7/main.c
index 96e53444967..5c7337ba642 100644
--- a/regression/cbmc/r_w_ok7/main.c
+++ b/regression/cbmc/r_w_ok7/main.c
@@ -4,8 +4,8 @@
 
 int main()
 {
-  size_t x;
-  size_t y;
+  size_t x = __VERIFIER_nondet_size_t();
+  size_t y = __VERIFIER_nondet_size_t();
   uint8_t *a;
 
   __CPROVER_assume(x > 0);
diff --git a/regression/cbmc/return4/main.c b/regression/cbmc/return4/main.c
index 21041246471..d6093df3e8d 100644
--- a/regression/cbmc/return4/main.c
+++ b/regression/cbmc/return4/main.c
@@ -69,7 +69,7 @@ short f1_wh(short x)
 
 int main()
 {
-  int flag;
+  int flag = __VERIFIER_nondet_int();
   short a;
   short res0, res1;
 
diff --git a/regression/cbmc/runtime-profiling/main.c b/regression/cbmc/runtime-profiling/main.c
index e5b6087864e..281d7289b6a 100644
--- a/regression/cbmc/runtime-profiling/main.c
+++ b/regression/cbmc/runtime-profiling/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int a;
+  int a = __VERIFIER_nondet_int();
   int temp = a;
   a = a + 1;
   assert(a == temp + 1);
diff --git a/regression/cbmc/sat-solver-warning/test.c b/regression/cbmc/sat-solver-warning/test.c
index 4127814cad1..e10accf4a50 100644
--- a/regression/cbmc/sat-solver-warning/test.c
+++ b/regression/cbmc/sat-solver-warning/test.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  unsigned x;
+  unsigned x = __VERIFIER_nondet_unsigned();
   unsigned y = x;
   x /= 2;
   y /= 2;
diff --git a/regression/cbmc/simplify-array-size/main.c b/regression/cbmc/simplify-array-size/main.c
index e25583325ad..b341b6eb3bc 100644
--- a/regression/cbmc/simplify-array-size/main.c
+++ b/regression/cbmc/simplify-array-size/main.c
@@ -15,7 +15,7 @@ struct hash_table
 void main(void)
 {
   struct hash_table map;
-  size_t num_entries;
+  size_t num_entries = __VERIFIER_nondet_size_t();
   __CPROVER_assume(num_entries <= 8ul);
   size_t required_bytes = num_entries * sizeof(int) + sizeof(struct state);
   struct state *impl = malloc(required_bytes);
diff --git a/regression/cbmc/struct1/main.c b/regression/cbmc/struct1/main.c
index efcfd7302a8..2f9df79e723 100644
--- a/regression/cbmc/struct1/main.c
+++ b/regression/cbmc/struct1/main.c
@@ -16,7 +16,8 @@ struct y {
 
 int main()
 {
-  struct y Y;
+  struct y nondet_y(void);
+  struct y Y = nondet_y();
 
   {
     struct x tmp;
diff --git a/regression/cbmc/struct3/main.c b/regression/cbmc/struct3/main.c
index 207a2e40da3..b3fa73e10f7 100644
--- a/regression/cbmc/struct3/main.c
+++ b/regression/cbmc/struct3/main.c
@@ -1,10 +1,15 @@
-int main() {
-  struct
-  {
-    int a, b;
-  } s, q;
+struct ab
+{
+  int a, b;
+};
 
-  s=q;
+struct ab nondet_ab(void);
 
-  assert(s.a==q.a);
+int main()
+{
+  struct ab s, q = nondet_ab();
+
+  s = q;
+
+  assert(s.a == q.a);
 }
diff --git a/regression/cbmc/struct7/main.c b/regression/cbmc/struct7/main.c
index 45c5798a48e..d5211149c7e 100644
--- a/regression/cbmc/struct7/main.c
+++ b/regression/cbmc/struct7/main.c
@@ -16,7 +16,7 @@ void f(int *p)
 
 int main()
 {
-  int ind, x;
+  int ind, x = __VERIFIER_nondet_int();
   ind=x;
   int *p=&s.array[ind];
 
diff --git a/regression/cbmc/struct8/main.c b/regression/cbmc/struct8/main.c
index c8e65e7bcd0..273e81e12ca 100644
--- a/regression/cbmc/struct8/main.c
+++ b/regression/cbmc/struct8/main.c
@@ -5,7 +5,8 @@ struct X
 
 int main()
 {
-  int aa, bb, cc;
+  int aa = __VERIFIER_nondet_int(), bb = __VERIFIER_nondet_int(),
+      cc = __VERIFIER_nondet_int();
 
   struct X foo;
 
diff --git a/regression/cbmc/switch1/main.c b/regression/cbmc/switch1/main.c
index cb69400a25d..bdb6391f1fa 100644
--- a/regression/cbmc/switch1/main.c
+++ b/regression/cbmc/switch1/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int i;
+  int i = __VERIFIER_nondet_int();
 
   switch(i)
   {
diff --git a/regression/cbmc/switch2/main.c b/regression/cbmc/switch2/main.c
index 41d8afa789d..792f8566ad9 100644
--- a/regression/cbmc/switch2/main.c
+++ b/regression/cbmc/switch2/main.c
@@ -14,7 +14,7 @@ int f(int j)
 
 int main()
 {
-  int i;
+  int i = __VERIFIER_nondet_int();
 
   __CPROVER_assume(i==3 || i==4);
 
diff --git a/regression/cbmc/switch4/main.c b/regression/cbmc/switch4/main.c
index b2337cbce06..2ea9336037e 100644
--- a/regression/cbmc/switch4/main.c
+++ b/regression/cbmc/switch4/main.c
@@ -1,6 +1,6 @@
 main()
 {
-  int x;
+  int x = __VERIFIER_nondet_int();
 
   switch(x)
   {
diff --git a/regression/cbmc/sync_X_and_fetch-1/main.c b/regression/cbmc/sync_X_and_fetch-1/main.c
index b77f0a690e1..2f728219a13 100644
--- a/regression/cbmc/sync_X_and_fetch-1/main.c
+++ b/regression/cbmc/sync_X_and_fetch-1/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int *p, v, x, x_before;
+  int *p, v = __VERIFIER_nondet_int(), x = __VERIFIER_nondet_int(), x_before;
   x_before = x;
   p = &x;
 
diff --git a/regression/cbmc/sync_bool_compare-1/main.c b/regression/cbmc/sync_bool_compare-1/main.c
index 20e4d86e3e7..39cc736fb30 100644
--- a/regression/cbmc/sync_bool_compare-1/main.c
+++ b/regression/cbmc/sync_bool_compare-1/main.c
@@ -2,7 +2,8 @@
 
 int main()
 {
-  int *p, o, n, x, x_before;
+  int *p, o = __VERIFIER_nondet_int(), n = __VERIFIER_nondet_int(),
+          x = __VERIFIER_nondet_int(), x_before;
   x_before = x;
   p = &x;
 
diff --git a/regression/cbmc/sync_fetch_and_X-1/main.c b/regression/cbmc/sync_fetch_and_X-1/main.c
index b643b45c3c9..f58568c2d99 100644
--- a/regression/cbmc/sync_fetch_and_X-1/main.c
+++ b/regression/cbmc/sync_fetch_and_X-1/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int *p, v, x, x_before;
+  int *p, v = __VERIFIER_nondet_int(), x = __VERIFIER_nondet_int(), x_before;
   x_before = x;
   p = &x;
 
diff --git a/regression/cbmc/sync_val_compare-1/main.c b/regression/cbmc/sync_val_compare-1/main.c
index 781298ea42e..226831f9b1c 100644
--- a/regression/cbmc/sync_val_compare-1/main.c
+++ b/regression/cbmc/sync_val_compare-1/main.c
@@ -2,7 +2,8 @@
 
 int main()
 {
-  int *p, o, n, x, x_before;
+  int *p, o = __VERIFIER_nondet_int(), n = __VERIFIER_nondet_int(),
+          x = __VERIFIER_nondet_int(), x_before;
   x_before = x;
   p = &x;
 
diff --git a/regression/cbmc/uniform_array1/main.c b/regression/cbmc/uniform_array1/main.c
index 1a7cd4389d7..605ed1cd5bd 100644
--- a/regression/cbmc/uniform_array1/main.c
+++ b/regression/cbmc/uniform_array1/main.c
@@ -1,7 +1,7 @@
 int main()
 {
   int A[] = {1, 1};
-  int i;
+  int i = __VERIFIER_nondet_int();
   __CPROVER_assert(i < 0 || i > 1 || A[i] == 1, "valid access into array of 1");
   __CPROVER_assert(A[i] == 1, "possible out-of-bounds access");
   return 0;
diff --git a/regression/cbmc/uninterpreted_function/uf2.c b/regression/cbmc/uninterpreted_function/uf2.c
index 9a1bf243c7c..959db83812a 100644
--- a/regression/cbmc/uninterpreted_function/uf2.c
+++ b/regression/cbmc/uninterpreted_function/uf2.c
@@ -3,7 +3,7 @@ __CPROVER_bool __CPROVER_uninterpreted_g(int, int);
 
 main()
 {
-  int a, b;
+  int a = __VERIFIER_nondet_int(), b = __VERIFIER_nondet_int();
 
   int inst1 = __CPROVER_uninterpreted_f(1, a);
   int inst2 = __CPROVER_uninterpreted_f(1, b);
diff --git a/regression/cbmc/union17/main.c b/regression/cbmc/union17/main.c
index 73d13b938d7..8c48e0e0801 100644
--- a/regression/cbmc/union17/main.c
+++ b/regression/cbmc/union17/main.c
@@ -1,7 +1,7 @@
 int main()
 {
   // create a union type of non-constant, non-zero size
-  unsigned x;
+  unsigned x = __VERIFIER_nondet_unsigned();
   __CPROVER_assume(x > 0);
   union U
   {
diff --git a/regression/cbmc/union3/main.c b/regression/cbmc/union3/main.c
index 7a255cf6ca4..661e3e0d40e 100644
--- a/regression/cbmc/union3/main.c
+++ b/regression/cbmc/union3/main.c
@@ -13,7 +13,7 @@ int my_func(int stat_loc)
 int main(void)
 {
   #ifdef __GNUC__
-  int x;
+  int x = __VERIFIER_nondet_int();
   assert(my_func(x)==x);
 
   union my_U
diff --git a/regression/cbmc/unwind_counters4/main.c b/regression/cbmc/unwind_counters4/main.c
index b7f1edafbad..5a16aaf3524 100644
--- a/regression/cbmc/unwind_counters4/main.c
+++ b/regression/cbmc/unwind_counters4/main.c
@@ -1,6 +1,6 @@
 int main()
 {
-  int x;
+  int x = __VERIFIER_nondet_int();
   int y;
 
   do
@@ -9,7 +9,7 @@ int main()
     goto label;
     x = 1; // dead code, makes sure the above goto is not removed
   label:;
-    _Bool nondet;
+    _Bool nondet = __VERIFIER_nondet__Bool();
     if(nondet)
       __CPROVER_assert(y != 10, "violated via first loop");
     else
diff --git a/regression/cbmc/void_pointer3/main.c b/regression/cbmc/void_pointer3/main.c
index 80637cf198f..24676c24d44 100644
--- a/regression/cbmc/void_pointer3/main.c
+++ b/regression/cbmc/void_pointer3/main.c
@@ -8,7 +8,8 @@ int main()
   // with the object:offset encoding we need to make sure the address arithmetic
   // below will only touch the offset part
   __CPROVER_assume(sizeof(unsigned char)<sizeof(void*));
-  unsigned char o1, o2;
+  unsigned char o1 = __VERIFIER_nondet_char(),
+                o2 = __VERIFIER_nondet_unsigned_char();
 
   p+=o1;
   q+=o2;