diff --git a/.travis.yml b/.travis.yml
index 410d916517b..9f0127c71f6 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -101,7 +101,6 @@ jobs:
             - g++-5
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -136,7 +135,6 @@ jobs:
             - libwww-perl
             - g++-5
             - libubsan0
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -165,7 +163,6 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -194,7 +191,6 @@ jobs:
             - g++-5
             - libstdc++-5-dev
             - libubsan0
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -220,7 +216,6 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-5
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -245,7 +240,6 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-7
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-7 bin/gcc
@@ -276,7 +270,6 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         # Use gcc/g++ 5 for tests, as Clang doesn't work yet
diff --git a/regression/cbmc/Float24/main.c b/regression/cbmc/Float24/main.i
similarity index 100%
rename from regression/cbmc/Float24/main.c
rename to regression/cbmc/Float24/main.i
diff --git a/regression/cbmc/Float24/test.desc b/regression/cbmc/Float24/test.desc
index 6a7c97325db..fbb546488c7 100644
--- a/regression/cbmc/Float24/test.desc
+++ b/regression/cbmc/Float24/test.desc
@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --win32 --xml-ui
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc/Malloc15/main.c b/regression/cbmc/Malloc15/main.i
similarity index 100%
rename from regression/cbmc/Malloc15/main.c
rename to regression/cbmc/Malloc15/main.i
diff --git a/regression/cbmc/Malloc15/test.desc b/regression/cbmc/Malloc15/test.desc
index f046159d042..a1b2c8b18ec 100644
--- a/regression/cbmc/Malloc15/test.desc
+++ b/regression/cbmc/Malloc15/test.desc
@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --32
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc/Malloc16/main.c b/regression/cbmc/Malloc16/main.i
similarity index 100%
rename from regression/cbmc/Malloc16/main.c
rename to regression/cbmc/Malloc16/main.i
diff --git a/regression/cbmc/Malloc16/test.desc b/regression/cbmc/Malloc16/test.desc
index f046159d042..a1b2c8b18ec 100644
--- a/regression/cbmc/Malloc16/test.desc
+++ b/regression/cbmc/Malloc16/test.desc
@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --32
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc/Pointer_Arithmetic12/main.c b/regression/cbmc/Pointer_Arithmetic12/main.i
similarity index 92%
rename from regression/cbmc/Pointer_Arithmetic12/main.c
rename to regression/cbmc/Pointer_Arithmetic12/main.i
index 6177b6f4f6f..7bcede27aff 100644
--- a/regression/cbmc/Pointer_Arithmetic12/main.c
+++ b/regression/cbmc/Pointer_Arithmetic12/main.i
@@ -1,6 +1,4 @@
-#include <stdint.h>
-
-#include <assert.h>
+typedef unsigned int uint32_t;
 
 uint32_t __stack[32];
 
@@ -98,35 +96,25 @@ int main()
   L_0x401_0: esp-=0x14;
   L_0x404_0: var15=ebp;
   L_0x404_1: var15-=0x4;
-#ifdef NONDET
-  L_0x404_2: *(uint32_t*)(var15)=nondet_uint();
-#else
   L_0x404_2: *(uint32_t*)(var15)=0xffffffff;
-#endif
   L_0x40b_0: var16=ebp;
   L_0x40b_1: var16-=0x4;
   L_0x40b_2: eax=*(uint32_t*)(var16);
   L_0x40e_0: *(uint32_t*)(esp)=eax;
   L_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
-#if 1
              uint32_t eax1=eax;
   C_0x3ff_0: ebp=esp;
   C_0x401_0: esp-=0x14;
   C_0x404_0: var15=ebp;
   C_0x404_1: var15-=0x4;
-#ifdef NONDET
-  C_0x404_2: *(uint32_t*)(var15)=nondet_uint();
-#else
   C_0x404_2: *(uint32_t*)(var15)=0xffffffff;
-#endif
   C_0x40b_0: var16=ebp;
   C_0x40b_1: var16-=0x4;
   C_0x40b_2: eax=*(uint32_t*)(var16);
   C_0x40e_0: *(uint32_t*)(esp)=eax;
   C_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
              uint32_t eax2=eax;
-             assert(eax2==eax1);
-#endif
+             __CPROVER_assert(eax2 == eax1, "");
   L_0x416_0: esp=ebp;
   L_0x416_1: ebp=*(uint32_t*)(esp);
   L_0x416_2: esp+=0x4;
diff --git a/regression/cbmc/Pointer_Arithmetic12/test.desc b/regression/cbmc/Pointer_Arithmetic12/test.desc
index 3de54602985..b3a154d150b 100644
--- a/regression/cbmc/Pointer_Arithmetic12/test.desc
+++ b/regression/cbmc/Pointer_Arithmetic12/test.desc
@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --32 --little-endian
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc/Pointer_array4/main.c b/regression/cbmc/Pointer_array4/main.i
similarity index 81%
rename from regression/cbmc/Pointer_array4/main.c
rename to regression/cbmc/Pointer_array4/main.i
index 5f0b37139d5..8552cb097fb 100644
--- a/regression/cbmc/Pointer_array4/main.c
+++ b/regression/cbmc/Pointer_array4/main.i
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main()
 {
   int arrayOfIntegers[] = {1, 2, 3};
@@ -8,6 +6,6 @@ int main()
   int iFirst=(int)pointer2FirstElem;
   int iThird=(int)pointer2ThirdElem;
   int addrDiff = iThird-iFirst;
-  assert(addrDiff == 2* sizeof(int));
+  __CPROVER_assert(addrDiff == 2* sizeof(int), "");
   return 0;
 }
diff --git a/regression/cbmc/Pointer_array4/test.desc b/regression/cbmc/Pointer_array4/test.desc
index 0098f266ed3..35cc9d3cd74 100644
--- a/regression/cbmc/Pointer_array4/test.desc
+++ b/regression/cbmc/Pointer_array4/test.desc
@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --32
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc/Pointer_byte_extract5/main.c b/regression/cbmc/Pointer_byte_extract5/main.i
similarity index 85%
rename from regression/cbmc/Pointer_byte_extract5/main.c
rename to regression/cbmc/Pointer_byte_extract5/main.i
index dd4758852b2..023e2197a8d 100644
--- a/regression/cbmc/Pointer_byte_extract5/main.c
+++ b/regression/cbmc/Pointer_byte_extract5/main.i
@@ -6,19 +6,14 @@ typedef union
   int b;
 } Union;
 
-#ifdef __GNUC__
-typedef struct
-{
-  int Count;
-  Union List[1];
-} __attribute__((packed)) Struct3;
-#else
+#pragma pack(push)
+#pragma pack(1)
 typedef struct
 {
   int Count;
   Union List[1];
 } Struct3;
-#endif
+#pragma pack(pop)
 
 int main()
 {
diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc
index f93bcf98401..36c5519b60c 100644
--- a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc
+++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc
@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --bounds-check --32 --no-simplify
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc
index ba7ae563823..48d0d5d9c53 100644
--- a/regression/cbmc/Pointer_byte_extract5/test.desc
+++ b/regression/cbmc/Pointer_byte_extract5/test.desc
@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --bounds-check --32
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc/Pointer_byte_extract8/main.c b/regression/cbmc/Pointer_byte_extract8/main.i
similarity index 100%
rename from regression/cbmc/Pointer_byte_extract8/main.c
rename to regression/cbmc/Pointer_byte_extract8/main.i
diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc
index 25368d1f99d..b23fa8bd0df 100644
--- a/regression/cbmc/Pointer_byte_extract8/test.desc
+++ b/regression/cbmc/Pointer_byte_extract8/test.desc
@@ -1,5 +1,5 @@
 KNOWNBUG
-main.c
+main.i
 --bounds-check --32 --no-simplify
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc/Struct_Padding1/main.c b/regression/cbmc/Struct_Padding1/main.i
similarity index 55%
rename from regression/cbmc/Struct_Padding1/main.c
rename to regression/cbmc/Struct_Padding1/main.i
index 5dd960bd6c4..94a1f70a18a 100644
--- a/regression/cbmc/Struct_Padding1/main.c
+++ b/regression/cbmc/Struct_Padding1/main.i
@@ -1,8 +1,3 @@
-#include <assert.h>
-
-#define STATIC_ASSERT(condition) \
-  int some_array##__LINE__[(condition) ? 1 : -1]
-
 struct my_struct1
 {
   int i;
@@ -40,22 +35,22 @@ struct my_struct3 {
    int i;
 } xx3= { 1, 2 };
 
-STATIC_ASSERT(sizeof(xx1)==4+1+3+4+4);
-STATIC_ASSERT(sizeof(xx2)==4+4+4+4);
+int some_array1[(sizeof(xx1)==4+1+3+4+4) ? 1 : -1];
+int some_array2[(sizeof(xx2)==4+4+4+4) ? 1 : -1];
 
 int main()
 {
-  assert(xx1.i==1);
-  assert(xx1.ch==2);
-  assert(xx1.j==3);
+  __CPROVER_assert(xx1.i==1, "");
+  __CPROVER_assert(xx1.ch==2, "");
+  __CPROVER_assert(xx1.j==3, "");
 
   // let's probe the padding
   char *p=&xx1.ch;
-  assert(p[0]==2);
-  assert(p[1]==0);
-  assert(p[2]==0);
-  assert(p[3]==0);
+  __CPROVER_assert(p[0]==2, "");
+  __CPROVER_assert(p[1]==0, "");
+  __CPROVER_assert(p[2]==0, "");
+  __CPROVER_assert(p[3]==0, "");
 
-  assert(xx3.bit_field==1);
-  assert(xx3.i==2);
+  __CPROVER_assert(xx3.bit_field==1, "");
+  __CPROVER_assert(xx3.i==2, "");
 }
diff --git a/regression/cbmc/Struct_Padding1/test.desc b/regression/cbmc/Struct_Padding1/test.desc
index 0098f266ed3..35cc9d3cd74 100644
--- a/regression/cbmc/Struct_Padding1/test.desc
+++ b/regression/cbmc/Struct_Padding1/test.desc
@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --32
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc/Visual_Studio_Types1/main.c b/regression/cbmc/Visual_Studio_Types1/main.c
deleted file mode 100644
index 48f37c2175f..00000000000
--- a/regression/cbmc/Visual_Studio_Types1/main.c
+++ /dev/null
@@ -1,48 +0,0 @@
-int main()
-{
-  // these types are Visual Studio-specific
-  #ifdef _MSC_VER
-  __int8 i1;
-  __int16 i2;
-  __int32 i3;
-  __int64 i4;
-
-  assert(sizeof(i1)==1);
-  assert(sizeof(i2)==2);
-  assert(sizeof(i3)==4);
-  assert(sizeof(i4)==8);
-  #endif
-
-  // general types
-
-  char c;
-  short s;
-  int i;
-  long l;
-  long long ll;
-
-  assert(sizeof(c)==1);
-  assert(sizeof(s)==2);
-  assert(sizeof(i)==4);
-  assert(sizeof(l)==4);
-  assert(sizeof(ll)==8);
-
-  // these constants are Visual Studio-specific
-  #ifdef _MSC_VER
-  assert(sizeof(1i8)==1);
-  assert(sizeof(1i16)==2);
-  assert(sizeof(1i32)==4);
-  assert(sizeof(1i64)==8);
-  assert(sizeof(1i128)==16);
-
-  // oh, and these pointer qualifiers are Visual Studio-specific
-  int * __ptr32 p32;
-  //int * __ptr64 p64;
-
-  // requires --i386-win32 to work
-  assert(sizeof(p32)==4);
-  //assert(sizeof(p64)==8);
-  #endif
-
-  assert(sizeof(void *)==4);
-}
diff --git a/regression/cbmc/Visual_Studio_Types1/main.i b/regression/cbmc/Visual_Studio_Types1/main.i
new file mode 100644
index 00000000000..ee394a32566
--- /dev/null
+++ b/regression/cbmc/Visual_Studio_Types1/main.i
@@ -0,0 +1,44 @@
+int main()
+{
+  // these types are Visual Studio-specific
+  __int8 i1;
+  __int16 i2;
+  __int32 i3;
+  __int64 i4;
+
+  __CPROVER_assert(sizeof(i1) == 1, "");
+  __CPROVER_assert(sizeof(i2) == 2, "");
+  __CPROVER_assert(sizeof(i3) == 4, "");
+  __CPROVER_assert(sizeof(i4) == 8, "");
+
+  // general types
+
+  char c;
+  short s;
+  int i;
+  long l;
+  long long ll;
+
+  __CPROVER_assert(sizeof(c) == 1, "");
+  __CPROVER_assert(sizeof(s) == 2, "");
+  __CPROVER_assert(sizeof(i) == 4, "");
+  __CPROVER_assert(sizeof(l) == 4, "");
+  __CPROVER_assert(sizeof(ll) == 8, "");
+
+  // these constants are Visual Studio-specific
+  __CPROVER_assert(sizeof(1i8) == 1, "");
+  __CPROVER_assert(sizeof(1i16) == 2, "");
+  __CPROVER_assert(sizeof(1i32) == 4, "");
+  __CPROVER_assert(sizeof(1i64) == 8, "");
+  __CPROVER_assert(sizeof(1i128) == 16, "");
+
+  // oh, and these pointer qualifiers are Visual Studio-specific
+  int * __ptr32 p32;
+  //int * __ptr64 p64;
+
+  // requires --i386-win32 to work
+  __CPROVER_assert(sizeof(p32) == 4, "");
+  //__CPROVER_assert(sizeof(p64) == 8, "");
+
+  __CPROVER_assert(sizeof(void *) == 4, "");
+}
diff --git a/regression/cbmc/Visual_Studio_Types1/test.desc b/regression/cbmc/Visual_Studio_Types1/test.desc
index e59b02c324d..982c46d6c98 100644
--- a/regression/cbmc/Visual_Studio_Types1/test.desc
+++ b/regression/cbmc/Visual_Studio_Types1/test.desc
@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --i386-win32
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc/Visual_Studio_Types2/main.c b/regression/cbmc/Visual_Studio_Types2/main.c
deleted file mode 100644
index 921143e24a6..00000000000
--- a/regression/cbmc/Visual_Studio_Types2/main.c
+++ /dev/null
@@ -1,25 +0,0 @@
-int main()
-{
-  // general types
-  short s;
-  int i;
-  long l;
-  long long ll;
-
-  assert(sizeof(s)==2);
-  assert(sizeof(i)==4);
-  assert(sizeof(l)==4);
-  assert(sizeof(ll)==8);
-
-  // oh, and these pointer qualifiers are MS-specific
-  #ifdef _MSC_VER
-  int * __ptr32 p32;
-  int * __ptr64 p64;
-
-  // requires --winx64 to work
-  assert(sizeof(p32)==4);
-  assert(sizeof(p64)==8);
-  #endif
-
-  assert(sizeof(void *)==8);
-}
diff --git a/regression/cbmc/Visual_Studio_Types2/main.i b/regression/cbmc/Visual_Studio_Types2/main.i
new file mode 100644
index 00000000000..7391910dfde
--- /dev/null
+++ b/regression/cbmc/Visual_Studio_Types2/main.i
@@ -0,0 +1,23 @@
+int main()
+{
+  // general types
+  short s;
+  int i;
+  long l;
+  long long ll;
+
+  __CPROVER_assert(sizeof(s) == 2, "");
+  __CPROVER_assert(sizeof(i) == 4, "");
+  __CPROVER_assert(sizeof(l) == 4, "");
+  __CPROVER_assert(sizeof(ll) == 8, "");
+
+  // oh, and these pointer qualifiers are MS-specific
+  int * __ptr32 p32;
+  int * __ptr64 p64;
+
+  // requires --winx64 to work
+  __CPROVER_assert(sizeof(p32) == 4, "");
+  __CPROVER_assert(sizeof(p64) == 8, "");
+
+  __CPROVER_assert(sizeof(void *) == 8, "");
+}
diff --git a/regression/cbmc/Visual_Studio_Types2/test.desc b/regression/cbmc/Visual_Studio_Types2/test.desc
index 7ce542782ab..254b9942989 100644
--- a/regression/cbmc/Visual_Studio_Types2/test.desc
+++ b/regression/cbmc/Visual_Studio_Types2/test.desc
@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --winx64
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc/address_space_size_limit2/test.desc b/regression/cbmc/address_space_size_limit2/test.desc
index 63d05de2268..0cb9a06b547 100644
--- a/regression/cbmc/address_space_size_limit2/test.desc
+++ b/regression/cbmc/address_space_size_limit2/test.desc
@@ -1,5 +1,5 @@
 KNOWNBUG
-test.c
+test.i
 --32 --object-bits 31 --unwind 11 --no-simplify
 dynamic object too large
 --
diff --git a/regression/cbmc/address_space_size_limit2/test.c b/regression/cbmc/address_space_size_limit2/test.i
similarity index 66%
rename from regression/cbmc/address_space_size_limit2/test.c
rename to regression/cbmc/address_space_size_limit2/test.i
index 1e7285d5191..1bbf09c3bbe 100644
--- a/regression/cbmc/address_space_size_limit2/test.c
+++ b/regression/cbmc/address_space_size_limit2/test.i
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void *malloc(__CPROVER_size_t);
 
 int main(int argc, char** argv)
@@ -7,5 +5,5 @@ int main(int argc, char** argv)
   char* c=(char*)malloc(10);
   char* d=c;
   for(char i=0; i<10; i++, d++);
-  assert((size_t)d==(size_t)c+10);
+  __CPROVER_assert((__CPROVER_size_t)d == (__CPROVER_size_t)c + 10, "");
 }
diff --git a/regression/cbmc/address_space_size_limit3/main.c b/regression/cbmc/address_space_size_limit3/main.i
similarity index 92%
rename from regression/cbmc/address_space_size_limit3/main.c
rename to regression/cbmc/address_space_size_limit3/main.i
index 6c62d538ee5..ab817d9e0bb 100644
--- a/regression/cbmc/address_space_size_limit3/main.c
+++ b/regression/cbmc/address_space_size_limit3/main.i
@@ -1,8 +1,6 @@
 // copy of Pointer_Arithmetic12
 
-#include <stdint.h>
-
-#include <assert.h>
+typedef unsigned int uint32_t;
 
 uint32_t __stack[32];
 
@@ -100,35 +98,25 @@ int main()
   L_0x401_0: esp-=0x14;
   L_0x404_0: var15=ebp;
   L_0x404_1: var15-=0x4;
-#ifdef NONDET
-  L_0x404_2: *(uint32_t*)(var15)=nondet_uint();
-#else
   L_0x404_2: *(uint32_t*)(var15)=0xffffffff;
-#endif
   L_0x40b_0: var16=ebp;
   L_0x40b_1: var16-=0x4;
   L_0x40b_2: eax=*(uint32_t*)(var16);
   L_0x40e_0: *(uint32_t*)(esp)=eax;
   L_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
-#if 1
              uint32_t eax1=eax;
   C_0x3ff_0: ebp=esp;
   C_0x401_0: esp-=0x14;
   C_0x404_0: var15=ebp;
   C_0x404_1: var15-=0x4;
-#ifdef NONDET
-  C_0x404_2: *(uint32_t*)(var15)=nondet_uint();
-#else
   C_0x404_2: *(uint32_t*)(var15)=0xffffffff;
-#endif
   C_0x40b_0: var16=ebp;
   C_0x40b_1: var16-=0x4;
   C_0x40b_2: eax=*(uint32_t*)(var16);
   C_0x40e_0: *(uint32_t*)(esp)=eax;
   C_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
              uint32_t eax2=eax;
-             assert(eax2==eax1);
-#endif
+             __CPROVER_assert(eax2 == eax1, "");
   L_0x416_0: esp=ebp;
   L_0x416_1: ebp=*(uint32_t*)(esp);
   L_0x416_2: esp+=0x4;
diff --git a/regression/cbmc/address_space_size_limit3/test.desc b/regression/cbmc/address_space_size_limit3/test.desc
index ee7b4e94ab8..ac8f72553aa 100644
--- a/regression/cbmc/address_space_size_limit3/test.desc
+++ b/regression/cbmc/address_space_size_limit3/test.desc
@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --32 --little-endian --object-bits 25 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$