diff --git a/appveyor.yml b/appveyor.yml
index ee24f7bcfb8..28749ffc5e6 100644
--- a/appveyor.yml
+++ b/appveyor.yml
@@ -90,6 +90,9 @@ test_script:
     rmdir /s /q cpp\Decltype1
     rmdir /s /q cpp\Decltype2
     rmdir /s /q cpp\Function_Overloading1
+    rmdir /s /q cpp\Resolver10
+    rmdir /s /q cpp\Resolver11
+    rmdir /s /q cpp\Template_Parameters1
     rmdir /s /q cpp\enum2
     rmdir /s /q cpp\enum7
     rmdir /s /q cpp\enum8
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
index d915af9cf1a..3b7423c5dbe 100644
--- a/regression/CMakeLists.txt
+++ b/regression/CMakeLists.txt
@@ -30,6 +30,7 @@ add_subdirectory(goto-instrument)
 add_subdirectory(cpp)
 add_subdirectory(cbmc-cover)
 add_subdirectory(goto-instrument-typedef)
+add_subdirectory(smt2_solver)
 add_subdirectory(strings)
 add_subdirectory(invariants)
 add_subdirectory(goto-diff)
@@ -41,4 +42,4 @@ endif()
 add_subdirectory(goto-cc-cbmc)
 add_subdirectory(cbmc-cpp)
 add_subdirectory(goto-cc-goto-analyzer)
-
+add_subdirectory(systemc)
diff --git a/regression/Makefile b/regression/Makefile
index 64972660142..c41b1080e89 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -18,6 +18,7 @@ DIRS = cbmc \
        goto-cc-cbmc \
        cbmc-cpp \
        goto-cc-goto-analyzer \
+       systemc
        # Empty last line
 
 # Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks
diff --git a/regression/cbmc/cpp1/main.cpp b/regression/cbmc/cpp1/main.cpp
new file mode 100644
index 00000000000..c41b16e0243
--- /dev/null
+++ b/regression/cbmc/cpp1/main.cpp
@@ -0,0 +1,48 @@
+#include <cassert>
+
+template <class T>
+class sc_signal
+{
+public:
+    T data;
+    sc_signal(){}
+    sc_signal(const char *p) {}
+    T read() {return data;}
+    void write(const T &d) {data = d;}
+};
+
+
+struct rbm
+{
+
+   sc_signal<unsigned int>  data_out;   //<L1>
+
+   sc_signal<bool>   done;  // <L2>
+
+   sc_signal<bool> conf_done;
+
+   void config();
+
+   rbm()
+   {
+
+   }
+
+};
+
+
+void rbm::config()
+{
+   do {
+         conf_done.write(true);
+         assert(conf_done.data==true);
+    } while ( !conf_done.read() );
+}
+
+int main()
+{
+    rbm IMPL;
+    IMPL.config();
+
+    return 0;
+}
diff --git a/regression/cbmc/cpp1/test.desc b/regression/cbmc/cpp1/test.desc
new file mode 100644
index 00000000000..7ad0d9caff4
--- /dev/null
+++ b/regression/cbmc/cpp1/test.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This has been reported as #661.
diff --git a/regression/cbmc/cpp2/main.cpp b/regression/cbmc/cpp2/main.cpp
new file mode 100644
index 00000000000..9f49a0da733
--- /dev/null
+++ b/regression/cbmc/cpp2/main.cpp
@@ -0,0 +1,47 @@
+#include <cassert>
+#include <stdint.h>
+#include <stdbool.h>
+
+#undef HOTFIX
+
+typedef struct {
+  uint32_t value_31_0 : 32;
+} signal32_t;
+
+typedef struct {
+  uint8_t value_0_0 : 1;
+} signal1_t;
+
+static inline bool yosys_simplec_get_bit_25_of_32(const signal32_t *sig)
+{
+  return (sig->value_31_0 >> 25) & 1;
+}
+
+struct rvfi_insn_srai_state_t
+{
+  signal32_t rvfi_insn;
+  signal32_t rvfi_rs1_rdata;
+  signal1_t _abc_1398_n364;
+  signal1_t _abc_1398_n363;
+};
+
+void test(rvfi_insn_srai_state_t state, bool valid)
+{
+#ifndef HOTFIX
+  state._abc_1398_n364.value_0_0 = yosys_simplec_get_bit_25_of_32(&state.rvfi_insn) ?
+      yosys_simplec_get_bit_25_of_32(&state.rvfi_rs1_rdata) : state._abc_1398_n363.value_0_0;
+#else
+  state._abc_1398_n364.value_0_0 = yosys_simplec_get_bit_25_of_32(&state.rvfi_insn) ?
+      yosys_simplec_get_bit_25_of_32(&state.rvfi_rs1_rdata) : (bool)state._abc_1398_n363.value_0_0;
+#endif
+
+  assert(valid);
+}
+
+int main(int argc, char* argv[])
+{
+	rvfi_insn_srai_state_t state;
+  bool valid;
+  test(state, valid);
+  return 0;
+}
diff --git a/regression/cbmc/cpp2/test.desc b/regression/cbmc/cpp2/test.desc
new file mode 100644
index 00000000000..eb6229bb599
--- /dev/null
+++ b/regression/cbmc/cpp2/test.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^equality without matching types
+--
+This has been reported as #933.
diff --git a/regression/cpp/Apple_extensions1/main.cpp b/regression/cpp/Apple_extensions1/main.cpp
index 1fc93e1ad7f..90d587123e6 100644
--- a/regression/cpp/Apple_extensions1/main.cpp
+++ b/regression/cpp/Apple_extensions1/main.cpp
@@ -5,3 +5,7 @@ void * _Nonnull p2;
 // block pointer
 void (^p3)(void);
 #endif
+
+int main(int argc, char* argv[])
+{
+}
diff --git a/regression/cpp/Apple_extensions1/test.desc b/regression/cpp/Apple_extensions1/test.desc
index a003b07b93c..a15d05875dc 100644
--- a/regression/cpp/Apple_extensions1/test.desc
+++ b/regression/cpp/Apple_extensions1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.cpp
 
 ^EXIT=0$
@@ -6,3 +6,5 @@ main.cpp
 --
 ^warning: ignoring
 ^CONVERSION ERROR$
+--
+This is being tracked in #1647.
diff --git a/regression/cpp/Constant2/main.cpp b/regression/cpp/Constant2/main.cpp
index 407ca855358..73de7bee948 100644
--- a/regression/cpp/Constant2/main.cpp
+++ b/regression/cpp/Constant2/main.cpp
@@ -1,3 +1,5 @@
+#include <cassert>
+
 int const C=10;
 
 int main()
diff --git a/regression/cpp/List_initialization1/main.cpp b/regression/cpp/List_initialization1/main.cpp
index 690461a7b0e..cf8d063a26e 100644
--- a/regression/cpp/List_initialization1/main.cpp
+++ b/regression/cpp/List_initialization1/main.cpp
@@ -26,7 +26,7 @@ int main()
   int y { 1 };
   x={ 1 };
   x=int { 1 };
-  x=(int) { 1 }
+  x=(int) { 1 };
   p=new int { 1 };
   some_function({1});
 }
diff --git a/regression/cpp/ModeC1/main.cpp b/regression/cpp/ModeC1/main.cpp
index 173242dd916..4af4d1fa736 100644
--- a/regression/cpp/ModeC1/main.cpp
+++ b/regression/cpp/ModeC1/main.cpp
@@ -1,5 +1,6 @@
 int cpp_f(int fkt_argument)
 {
+  return 0;
 }
 
 extern "C" void f(int fkt_argument)
@@ -27,4 +28,6 @@ int main()
   f(0);
   g(0);
   g(0L);
+
+  return 0;
 }
diff --git a/regression/cpp/Qualifiers_In_Template_Specialisation1/main.cpp b/regression/cpp/Qualifiers_In_Template_Specialisation1/main.cpp
index 20af2cb6769..046a14dbad8 100644
--- a/regression/cpp/Qualifiers_In_Template_Specialisation1/main.cpp
+++ b/regression/cpp/Qualifiers_In_Template_Specialisation1/main.cpp
@@ -1,5 +1,6 @@
 template <class T>
 class c {
+public:
   void fun (const T &arg);
 };
 
@@ -9,7 +10,7 @@ void c<long int>::fun (const long int &arg) { return; }
 int main(void) {
   c<long int> cl;
 
-  cl.fun();
+  cl.fun(0);
 
   return 0;
 }
diff --git a/regression/cpp/Resolver10/main.cpp b/regression/cpp/Resolver10/main.cpp
index e27e8524bf9..449bba39f65 100644
--- a/regression/cpp/Resolver10/main.cpp
+++ b/regression/cpp/Resolver10/main.cpp
@@ -1,3 +1,5 @@
+#include <cassert>
+
 struct A
 {
   int i;
@@ -10,7 +12,7 @@ struct B: A
   {
     i = 1;
     A();
-    assert(i==1);
+    __CPROVER_assert(i==1, "");
   }
 };
 
diff --git a/regression/cpp/Resolver11/main.cpp b/regression/cpp/Resolver11/main.cpp
index d6c6bc7fefc..5d503db7b0e 100644
--- a/regression/cpp/Resolver11/main.cpp
+++ b/regression/cpp/Resolver11/main.cpp
@@ -1,3 +1,5 @@
+#include <cassert>
+
 struct A
 {
   bool func() { return false; }
@@ -17,7 +19,7 @@ struct A
 int main()
 {
   A a;
-  assert(a.test()==false);
+  __CPROVER_assert(a.test() == false, "");
   const A a2;
-  assert(a2.test()==true);
+  __CPROVER_assert(a2.test() == true, "");
 }
diff --git a/regression/cpp/Template_Instantiation2/main.cpp b/regression/cpp/Template_Instantiation2/main.cpp
index 244d242732e..bc3abcef9ca 100644
--- a/regression/cpp/Template_Instantiation2/main.cpp
+++ b/regression/cpp/Template_Instantiation2/main.cpp
@@ -6,3 +6,8 @@ public :
 
 template<>
 int c<char>::f00(const char*);
+
+int main(int argc, char* argv[])
+{
+  return 0;
+}
diff --git a/regression/cpp/Template_Parameters1/main.ii b/regression/cpp/Template_Parameters1/main.cpp
similarity index 67%
rename from regression/cpp/Template_Parameters1/main.ii
rename to regression/cpp/Template_Parameters1/main.cpp
index 3b06958235b..b16c1a5eb34 100644
--- a/regression/cpp/Template_Parameters1/main.ii
+++ b/regression/cpp/Template_Parameters1/main.cpp
@@ -1,3 +1,5 @@
+#include <cassert>
+
 // V depends on Ty
 template<typename Ty, Ty V>
 class T
@@ -10,6 +12,6 @@ T<int, 10> some_T;
 
 int main()
 {
-  assert(some_T.value==10);
+  __CPROVER_assert(some_T.value == 10, "");
 }
 
diff --git a/regression/cpp/Template_Parameters1/test.desc b/regression/cpp/Template_Parameters1/test.desc
index 00e7b725a0f..1567bd1e5d4 100644
--- a/regression/cpp/Template_Parameters1/test.desc
+++ b/regression/cpp/Template_Parameters1/test.desc
@@ -1,5 +1,5 @@
 CORE
-main.ii
+main.cpp
 
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cpp/Template_Specialisation2/main.ii b/regression/cpp/Template_Specialisation2/main.ii
index 3f882d0f11b..57e787011f0 100644
--- a/regression/cpp/Template_Specialisation2/main.ii
+++ b/regression/cpp/Template_Specialisation2/main.ii
@@ -15,3 +15,6 @@ struct __member_pointer_traits_imp<_Rp (_Class::*)() const>
 {
 };
 
+int main(int argc, char* argv[])
+{
+}
diff --git a/regression/cpp/Trailing_Return_Type1/test.desc b/regression/cpp/Trailing_Return_Type1/test.desc
index 1567bd1e5d4..08c77bc8bf5 100644
--- a/regression/cpp/Trailing_Return_Type1/test.desc
+++ b/regression/cpp/Trailing_Return_Type1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.cpp
-
+-std=c++11
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cpp/auto1/test.desc b/regression/cpp/auto1/test.desc
index 5893356edf6..0daa9695017 100644
--- a/regression/cpp/auto1/test.desc
+++ b/regression/cpp/auto1/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.cpp
-
+-std=c++11
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cpp/enum8/test.desc b/regression/cpp/enum8/test.desc
index f935f5ace1b..3862862ffd3 100644
--- a/regression/cpp/enum8/test.desc
+++ b/regression/cpp/enum8/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.cpp
---std=c++11
+-std=c++11
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cpp/sizeof2/main.cpp b/regression/cpp/sizeof2/main.cpp
index 3b132135845..2cac6d9655e 100644
--- a/regression/cpp/sizeof2/main.cpp
+++ b/regression/cpp/sizeof2/main.cpp
@@ -5,9 +5,12 @@ template <class T>
 int size()
 {
   sizeof(T);
+  return 0;
 }
 
 int main()
 {
   size<int>();
+
+  return 0;
 }
diff --git a/regression/cpp/type_traits_essentials1/main.cpp b/regression/cpp/type_traits_essentials1/main.cpp
index d6dc32cd51e..bdd5baf5417 100644
--- a/regression/cpp/type_traits_essentials1/main.cpp
+++ b/regression/cpp/type_traits_essentials1/main.cpp
@@ -55,6 +55,6 @@ class X
 
 int main(int argc, char* argv[])
 {
-  X<> x;
+  X<true> x;
   return x.val()?0:1;
 }
diff --git a/regression/cpp/type_traits_essentials1/test.desc b/regression/cpp/type_traits_essentials1/test.desc
index 5893356edf6..0daa9695017 100644
--- a/regression/cpp/type_traits_essentials1/test.desc
+++ b/regression/cpp/type_traits_essentials1/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.cpp
-
+-std=c++11
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cpp/typecast_ambiguity2/main.cpp b/regression/cpp/typecast_ambiguity2/main.cpp
index 47fca7cb8e1..b268770402e 100644
--- a/regression/cpp/typecast_ambiguity2/main.cpp
+++ b/regression/cpp/typecast_ambiguity2/main.cpp
@@ -5,6 +5,7 @@ int foo(int)
 
 unsigned some_function(void)
 {
+  return 0;
 }
 
 int main()
diff --git a/regression/cpp/virtual1/main.cpp b/regression/cpp/virtual1/main.cpp
index ab787903597..911f5550588 100644
--- a/regression/cpp/virtual1/main.cpp
+++ b/regression/cpp/virtual1/main.cpp
@@ -1,4 +1,6 @@
-#include <stdio.h>
+#include <cassert>
+#include <cstdio>
+
 class base
 {
 public:
@@ -26,7 +28,7 @@ int main (void)
     base* D = new derived;
     int a = D->func();
     delete D;
-    __CPROVER_assert(a == 2, "Property 1");
+    assert(a == 2);
     return a;
 }
 
diff --git a/regression/smt2_solver/CMakeLists.txt b/regression/smt2_solver/CMakeLists.txt
new file mode 100644
index 00000000000..5a4bad9c15d
--- /dev/null
+++ b/regression/smt2_solver/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:smt2_solver>"
+)
diff --git a/regression/systemc/Array1/main.cpp b/regression/systemc/Array1/main.cpp
new file mode 100644
index 00000000000..aa6f4492308
--- /dev/null
+++ b/regression/systemc/Array1/main.cpp
@@ -0,0 +1,78 @@
+#include <assert.h>
+
+#define COPY
+
+typedef unsigned uint;
+
+template <class T, uint m>
+class myarray {
+
+  T elt[m];
+
+public:
+#if 0
+  myarray &operator=(const myarray &other) {
+    for (int i=0; i<m; i++) {
+      elt[i] = other.elt[i];
+    }
+    return *this;
+  }
+#endif
+
+  T& operator[] (int idx) {
+    return elt[idx];
+  }
+};
+
+#ifdef COPY
+myarray<uint, 3> rev3u(myarray<uint, 3> x) {
+  myarray<uint, 3> y;
+  y[0] = x[2];
+  y[1] = x[1];
+  y[2] = x[0];
+  return y;
+}
+
+#else
+
+void rev3u(myarray<uint, 3> x, myarray<uint, 3> &y) {
+  y[0] = x[2];
+  y[1] = x[1];
+  y[2] = x[0];
+}
+#endif
+
+extern bool arbb();
+extern uint arbu();
+
+int main(void) {
+  myarray<bool, 4> arrb;
+
+  for (int i=0; i<4; i++) {
+    bool cond = (i%2 == 0);
+    arrb[i] = cond;
+  }
+
+  assert(arrb[0] == true);
+  assert(arrb[1] == false);
+  assert(arrb[2] == true);
+  assert(arrb[3] == false);
+
+  myarray<uint, 3> arru;
+  for (int i=0; i<3; i++) {
+    arru[i] = arbu();
+  }
+
+  myarray<uint, 3> arru2;
+#ifdef COPY
+  arru2 = rev3u(arru); //problem: copy constructor refuses to copy array (solved)
+                       //new problem: byte_extract_little_endian ignored
+#else
+  rev3u(arru,arru2);
+#endif
+  assert (arru2[0] == arru[2]);
+  assert (arru2[1] == arru[1]);
+  assert (arru2[2] == arru[0]);
+
+  return 0;
+}
diff --git a/regression/systemc/Array1/test.desc b/regression/systemc/Array1/test.desc
new file mode 100644
index 00000000000..839148c295a
--- /dev/null
+++ b/regression/systemc/Array1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+-DNO_IO -DNO_STRING
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/Array1/tuple.h b/regression/systemc/Array1/tuple.h
new file mode 100644
index 00000000000..388ae0020f7
--- /dev/null
+++ b/regression/systemc/Array1/tuple.h
@@ -0,0 +1,171 @@
+
+#ifndef TUPLE_H
+#define TUPLE_H
+
+#define DECLARE_INSIDE
+
+#ifndef NO_IO
+#include <iostream>
+#endif
+
+// ---------------------------------------------------------------------
+// Templates for passing & returning tuples
+
+// null type
+struct null_type {};
+
+// a const value of null_type
+inline const null_type cnull() {return null_type();}
+
+#ifndef NO_IO
+std::ostream& operator<<(std::ostream& os, const null_type dummy)
+{
+  os << "-";
+  return os;
+}
+#endif
+
+// a global to absorb "writes" to unused tuple fields.
+// would be good to get rid of this.
+null_type dummy;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class ltuple;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class tuple
+{
+
+  T0 el0;
+  T1 el1;
+  T2 el2;
+  T3 el3;
+
+public:
+
+  friend tuple<T0,T1,T2,T3>
+  ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3>);
+
+#ifndef NO_IO
+  std::ostream&
+  dump (std::ostream& os) {
+    os << "(" << el0 << "," << el1 << "," << el2 << "," << el3 << ")";
+    return os;
+  }
+#endif
+
+  tuple() {}
+
+  tuple(T0 t0): el0(t0), el1(cnull()), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1): el0(t0), el1(t1), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2): el0(t0), el1(t1), el2(t2), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2, T3 t3): el0(t0), el1(t1), el2(t2), el3(t3) {}
+
+};
+
+#ifndef NO_IO
+template<class T0, class T1, class T2, class T3>
+  std::ostream& operator<<(std::ostream& os, tuple<T0,T1,T2,T3> src)
+{
+  return src.dump(os);
+}
+#endif
+
+template
+   <class T0,
+    class T1,
+    class T2,
+    class T3>
+class ltuple
+{
+
+private:
+  T0 &el0;
+  T1 &el1;
+  T2 &el2;
+  T3 &el3;
+
+public:
+
+#ifdef DECLARE_INSIDE
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+    : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src)
+    {
+      el0 = src.el0;
+      el1 = src.el1;
+      el2 = src.el2;
+      el3 = src.el3;
+      return src;
+    }
+#else
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 );
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src);
+#endif
+};
+
+
+#ifndef DECLARE_INSIDE
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>::ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+  : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+template <class T0, class T1, class T2, class T3>
+tuple<T0,T1,T2,T3>
+ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3> src)
+{
+  el0 = src.el0;
+  el1 = src.el1;
+  el2 = src.el2;
+  el3 = src.el3;
+  return src;
+}
+#endif
+
+template <class T0>
+ltuple<T0>
+tie(T0 &t0)
+{
+  return ltuple<T0>(t0, dummy, dummy, dummy);
+}
+
+template <class T0, class T1>
+ltuple<T0,T1>
+tie(T0 &t0, T1 &t1)
+{
+  return ltuple<T0,T1>(t0,t1,dummy,dummy);
+}
+
+template <class T0, class T1, class T2>
+ltuple<T0,T1,T2>
+tie(T0 &t0, T1 &t1, T2 &t2)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,dummy);
+}
+
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>
+tie(T0 &t0, T1 &t1, T2 &t2, T3 &t3)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,t3);
+}
+
+#endif
+
diff --git a/regression/systemc/Array2/main.cpp b/regression/systemc/Array2/main.cpp
new file mode 100644
index 00000000000..430ecce52b7
--- /dev/null
+++ b/regression/systemc/Array2/main.cpp
@@ -0,0 +1,28 @@
+#include <assert.h>
+
+class myarray {
+
+  int elt[4];
+
+public:
+  int& operator[] (int idx) {
+    return elt[idx];
+  }
+};
+
+int main(void) {
+  myarray x;
+
+  for (int i=0; i<4; i++) {
+    x[i] = i;
+  }
+
+  assert(x[0] == 0);
+  assert(x[3] == 3);
+
+  myarray y = x; //copy constructor does not typecheck
+  assert(y[0] == 0);
+  assert(y[3] == 3);
+
+  return 0;
+}
diff --git a/regression/systemc/Array2/test.desc b/regression/systemc/Array2/test.desc
new file mode 100644
index 00000000000..839148c295a
--- /dev/null
+++ b/regression/systemc/Array2/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+-DNO_IO -DNO_STRING
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/Array2/tuple.h b/regression/systemc/Array2/tuple.h
new file mode 100644
index 00000000000..388ae0020f7
--- /dev/null
+++ b/regression/systemc/Array2/tuple.h
@@ -0,0 +1,171 @@
+
+#ifndef TUPLE_H
+#define TUPLE_H
+
+#define DECLARE_INSIDE
+
+#ifndef NO_IO
+#include <iostream>
+#endif
+
+// ---------------------------------------------------------------------
+// Templates for passing & returning tuples
+
+// null type
+struct null_type {};
+
+// a const value of null_type
+inline const null_type cnull() {return null_type();}
+
+#ifndef NO_IO
+std::ostream& operator<<(std::ostream& os, const null_type dummy)
+{
+  os << "-";
+  return os;
+}
+#endif
+
+// a global to absorb "writes" to unused tuple fields.
+// would be good to get rid of this.
+null_type dummy;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class ltuple;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class tuple
+{
+
+  T0 el0;
+  T1 el1;
+  T2 el2;
+  T3 el3;
+
+public:
+
+  friend tuple<T0,T1,T2,T3>
+  ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3>);
+
+#ifndef NO_IO
+  std::ostream&
+  dump (std::ostream& os) {
+    os << "(" << el0 << "," << el1 << "," << el2 << "," << el3 << ")";
+    return os;
+  }
+#endif
+
+  tuple() {}
+
+  tuple(T0 t0): el0(t0), el1(cnull()), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1): el0(t0), el1(t1), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2): el0(t0), el1(t1), el2(t2), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2, T3 t3): el0(t0), el1(t1), el2(t2), el3(t3) {}
+
+};
+
+#ifndef NO_IO
+template<class T0, class T1, class T2, class T3>
+  std::ostream& operator<<(std::ostream& os, tuple<T0,T1,T2,T3> src)
+{
+  return src.dump(os);
+}
+#endif
+
+template
+   <class T0,
+    class T1,
+    class T2,
+    class T3>
+class ltuple
+{
+
+private:
+  T0 &el0;
+  T1 &el1;
+  T2 &el2;
+  T3 &el3;
+
+public:
+
+#ifdef DECLARE_INSIDE
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+    : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src)
+    {
+      el0 = src.el0;
+      el1 = src.el1;
+      el2 = src.el2;
+      el3 = src.el3;
+      return src;
+    }
+#else
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 );
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src);
+#endif
+};
+
+
+#ifndef DECLARE_INSIDE
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>::ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+  : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+template <class T0, class T1, class T2, class T3>
+tuple<T0,T1,T2,T3>
+ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3> src)
+{
+  el0 = src.el0;
+  el1 = src.el1;
+  el2 = src.el2;
+  el3 = src.el3;
+  return src;
+}
+#endif
+
+template <class T0>
+ltuple<T0>
+tie(T0 &t0)
+{
+  return ltuple<T0>(t0, dummy, dummy, dummy);
+}
+
+template <class T0, class T1>
+ltuple<T0,T1>
+tie(T0 &t0, T1 &t1)
+{
+  return ltuple<T0,T1>(t0,t1,dummy,dummy);
+}
+
+template <class T0, class T1, class T2>
+ltuple<T0,T1,T2>
+tie(T0 &t0, T1 &t1, T2 &t2)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,dummy);
+}
+
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>
+tie(T0 &t0, T1 &t1, T2 &t2, T3 &t3)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,t3);
+}
+
+#endif
+
diff --git a/regression/systemc/Array3/main.cpp b/regression/systemc/Array3/main.cpp
new file mode 100644
index 00000000000..3da119c53e5
--- /dev/null
+++ b/regression/systemc/Array3/main.cpp
@@ -0,0 +1,43 @@
+#include <assert.h>
+
+#define FUNCTION
+
+template<int m>
+class myarray {
+
+  int elt[m];
+
+public:
+  int& operator[] (int idx) {
+    return elt[idx];
+  }
+};
+
+#ifdef FUNCTION
+void check(myarray<4> &y)
+{
+  assert(y[0] == 0);
+  assert(y[3] == 3);
+}
+#endif
+
+int main(void) {
+  myarray<4> x;
+
+  for (int i=0; i<4; i++) {
+    x[i] = i;
+  }
+
+  assert(x[0] == 0);
+  assert(x[3] == 3);
+
+#ifdef FUNCTION
+  check(x); //this doesn't work
+#else
+  myarray<4> &y = x; //this works
+  assert(y[0] == 0);
+  assert(y[3] == 3);
+#endif
+
+  return 0;
+}
diff --git a/regression/systemc/Array3/test.desc b/regression/systemc/Array3/test.desc
new file mode 100644
index 00000000000..839148c295a
--- /dev/null
+++ b/regression/systemc/Array3/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+-DNO_IO -DNO_STRING
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/Array3/tuple.h b/regression/systemc/Array3/tuple.h
new file mode 100644
index 00000000000..388ae0020f7
--- /dev/null
+++ b/regression/systemc/Array3/tuple.h
@@ -0,0 +1,171 @@
+
+#ifndef TUPLE_H
+#define TUPLE_H
+
+#define DECLARE_INSIDE
+
+#ifndef NO_IO
+#include <iostream>
+#endif
+
+// ---------------------------------------------------------------------
+// Templates for passing & returning tuples
+
+// null type
+struct null_type {};
+
+// a const value of null_type
+inline const null_type cnull() {return null_type();}
+
+#ifndef NO_IO
+std::ostream& operator<<(std::ostream& os, const null_type dummy)
+{
+  os << "-";
+  return os;
+}
+#endif
+
+// a global to absorb "writes" to unused tuple fields.
+// would be good to get rid of this.
+null_type dummy;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class ltuple;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class tuple
+{
+
+  T0 el0;
+  T1 el1;
+  T2 el2;
+  T3 el3;
+
+public:
+
+  friend tuple<T0,T1,T2,T3>
+  ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3>);
+
+#ifndef NO_IO
+  std::ostream&
+  dump (std::ostream& os) {
+    os << "(" << el0 << "," << el1 << "," << el2 << "," << el3 << ")";
+    return os;
+  }
+#endif
+
+  tuple() {}
+
+  tuple(T0 t0): el0(t0), el1(cnull()), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1): el0(t0), el1(t1), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2): el0(t0), el1(t1), el2(t2), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2, T3 t3): el0(t0), el1(t1), el2(t2), el3(t3) {}
+
+};
+
+#ifndef NO_IO
+template<class T0, class T1, class T2, class T3>
+  std::ostream& operator<<(std::ostream& os, tuple<T0,T1,T2,T3> src)
+{
+  return src.dump(os);
+}
+#endif
+
+template
+   <class T0,
+    class T1,
+    class T2,
+    class T3>
+class ltuple
+{
+
+private:
+  T0 &el0;
+  T1 &el1;
+  T2 &el2;
+  T3 &el3;
+
+public:
+
+#ifdef DECLARE_INSIDE
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+    : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src)
+    {
+      el0 = src.el0;
+      el1 = src.el1;
+      el2 = src.el2;
+      el3 = src.el3;
+      return src;
+    }
+#else
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 );
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src);
+#endif
+};
+
+
+#ifndef DECLARE_INSIDE
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>::ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+  : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+template <class T0, class T1, class T2, class T3>
+tuple<T0,T1,T2,T3>
+ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3> src)
+{
+  el0 = src.el0;
+  el1 = src.el1;
+  el2 = src.el2;
+  el3 = src.el3;
+  return src;
+}
+#endif
+
+template <class T0>
+ltuple<T0>
+tie(T0 &t0)
+{
+  return ltuple<T0>(t0, dummy, dummy, dummy);
+}
+
+template <class T0, class T1>
+ltuple<T0,T1>
+tie(T0 &t0, T1 &t1)
+{
+  return ltuple<T0,T1>(t0,t1,dummy,dummy);
+}
+
+template <class T0, class T1, class T2>
+ltuple<T0,T1,T2>
+tie(T0 &t0, T1 &t1, T2 &t2)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,dummy);
+}
+
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>
+tie(T0 &t0, T1 &t1, T2 &t2, T3 &t3)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,t3);
+}
+
+#endif
+
diff --git a/regression/systemc/Array4/main.cpp b/regression/systemc/Array4/main.cpp
new file mode 100644
index 00000000000..73763c3b5ee
--- /dev/null
+++ b/regression/systemc/Array4/main.cpp
@@ -0,0 +1,49 @@
+#include <assert.h>
+
+#define CLASS
+
+#ifdef CLASS
+class myarray {
+
+  typedef bool base;
+  base elt[4];
+
+public:
+  base &operator[] (int idx) {
+    return elt[idx];
+  }
+};
+
+#else
+
+bool &get(bool *arr, int i)
+{
+  return arr[i];
+}
+#endif
+
+int main(void) {
+
+#ifndef CLASS
+  bool arrb[4];
+
+  for (int i=0; i<4; i++) {
+    bool cond = (i%2 == 0);
+    arrb[i] = cond;
+  }
+
+  assert(get(arrb,0) == true);
+
+#else
+
+  myarray arrb;
+
+  for (int i=0; i<4; i++) {
+    bool cond = (i%2 == 0);
+    arrb[i] = cond;
+  }
+
+  assert(arrb[2] == true);
+#endif
+  return 0;
+}
diff --git a/regression/systemc/Array4/test.desc b/regression/systemc/Array4/test.desc
new file mode 100644
index 00000000000..d091759e812
--- /dev/null
+++ b/regression/systemc/Array4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.cpp
+-DNO_IO -DNO_STRING
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/Array4/tuple.h b/regression/systemc/Array4/tuple.h
new file mode 100644
index 00000000000..388ae0020f7
--- /dev/null
+++ b/regression/systemc/Array4/tuple.h
@@ -0,0 +1,171 @@
+
+#ifndef TUPLE_H
+#define TUPLE_H
+
+#define DECLARE_INSIDE
+
+#ifndef NO_IO
+#include <iostream>
+#endif
+
+// ---------------------------------------------------------------------
+// Templates for passing & returning tuples
+
+// null type
+struct null_type {};
+
+// a const value of null_type
+inline const null_type cnull() {return null_type();}
+
+#ifndef NO_IO
+std::ostream& operator<<(std::ostream& os, const null_type dummy)
+{
+  os << "-";
+  return os;
+}
+#endif
+
+// a global to absorb "writes" to unused tuple fields.
+// would be good to get rid of this.
+null_type dummy;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class ltuple;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class tuple
+{
+
+  T0 el0;
+  T1 el1;
+  T2 el2;
+  T3 el3;
+
+public:
+
+  friend tuple<T0,T1,T2,T3>
+  ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3>);
+
+#ifndef NO_IO
+  std::ostream&
+  dump (std::ostream& os) {
+    os << "(" << el0 << "," << el1 << "," << el2 << "," << el3 << ")";
+    return os;
+  }
+#endif
+
+  tuple() {}
+
+  tuple(T0 t0): el0(t0), el1(cnull()), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1): el0(t0), el1(t1), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2): el0(t0), el1(t1), el2(t2), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2, T3 t3): el0(t0), el1(t1), el2(t2), el3(t3) {}
+
+};
+
+#ifndef NO_IO
+template<class T0, class T1, class T2, class T3>
+  std::ostream& operator<<(std::ostream& os, tuple<T0,T1,T2,T3> src)
+{
+  return src.dump(os);
+}
+#endif
+
+template
+   <class T0,
+    class T1,
+    class T2,
+    class T3>
+class ltuple
+{
+
+private:
+  T0 &el0;
+  T1 &el1;
+  T2 &el2;
+  T3 &el3;
+
+public:
+
+#ifdef DECLARE_INSIDE
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+    : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src)
+    {
+      el0 = src.el0;
+      el1 = src.el1;
+      el2 = src.el2;
+      el3 = src.el3;
+      return src;
+    }
+#else
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 );
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src);
+#endif
+};
+
+
+#ifndef DECLARE_INSIDE
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>::ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+  : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+template <class T0, class T1, class T2, class T3>
+tuple<T0,T1,T2,T3>
+ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3> src)
+{
+  el0 = src.el0;
+  el1 = src.el1;
+  el2 = src.el2;
+  el3 = src.el3;
+  return src;
+}
+#endif
+
+template <class T0>
+ltuple<T0>
+tie(T0 &t0)
+{
+  return ltuple<T0>(t0, dummy, dummy, dummy);
+}
+
+template <class T0, class T1>
+ltuple<T0,T1>
+tie(T0 &t0, T1 &t1)
+{
+  return ltuple<T0,T1>(t0,t1,dummy,dummy);
+}
+
+template <class T0, class T1, class T2>
+ltuple<T0,T1,T2>
+tie(T0 &t0, T1 &t1, T2 &t2)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,dummy);
+}
+
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>
+tie(T0 &t0, T1 &t1, T2 &t2, T3 &t3)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,t3);
+}
+
+#endif
+
diff --git a/regression/systemc/BitvectorC1/main.c b/regression/systemc/BitvectorC1/main.c
new file mode 100644
index 00000000000..d0416e6946d
--- /dev/null
+++ b/regression/systemc/BitvectorC1/main.c
@@ -0,0 +1,58 @@
+#include <assert.h>
+
+#define WIDTH 10
+
+signed __CPROVER_bitvector[WIDTH] add(signed __CPROVER_bitvector[WIDTH] a, signed __CPROVER_bitvector[WIDTH] b)
+{
+  return a+b;
+}
+
+int main(int argc, char** argv)
+{
+  unsigned __CPROVER_bitvector[WIDTH] x;
+  x = 1;
+  unsigned __CPROVER_bitvector[WIDTH] y = 2;
+
+  unsigned __CPROVER_bitvector[WIDTH] z = 0;
+  z += x;
+  z += y;
+
+  unsigned __CPROVER_bitvector[WIDTH] w = 3;
+  assert(z == w);
+
+  assert(add(-x,-y) == -w);
+
+  {
+    unsigned __CPROVER_bitvector[5] a = 30;
+    unsigned __CPROVER_bitvector[3] b;
+    unsigned __CPROVER_bitvector[3] c = 6;
+    b = a;
+    assert(b == c);
+  }
+
+  {
+    unsigned __CPROVER_bitvector[3] a = 6;
+    unsigned __CPROVER_bitvector[5] b;
+    unsigned __CPROVER_bitvector[5] c = 6;
+    b = a;
+    assert(b == c);
+  }
+
+  {
+    signed __CPROVER_bitvector[5] a = 30;
+    signed __CPROVER_bitvector[3] b;
+    signed __CPROVER_bitvector[3] c = -2;
+    b = a; //just truncated
+    assert(b == c);
+  }
+
+  {
+    signed __CPROVER_bitvector[3] a = -2;
+    signed __CPROVER_bitvector[5] b;
+    signed __CPROVER_bitvector[5] c = -2;
+    b = a; //sign gets extended
+    assert(b == c);
+  }
+
+  return 0;
+}
diff --git a/regression/systemc/BitvectorC1/test.desc b/regression/systemc/BitvectorC1/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/systemc/BitvectorC1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/BitvectorCpp1/main.cpp b/regression/systemc/BitvectorCpp1/main.cpp
new file mode 100644
index 00000000000..858aab0b5db
--- /dev/null
+++ b/regression/systemc/BitvectorCpp1/main.cpp
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main(int argc, char** argv)
+{
+  __CPROVER::signedbv<10> x;
+  x = 1;
+  __CPROVER::signedbv<10> y = 2;
+
+  __CPROVER::signedbv<10> z = 0;
+  z += x;
+  z += y;
+
+  __CPROVER::signedbv<10> w = 3;
+  assert(z == w);
+
+  return 0;
+}
diff --git a/regression/systemc/BitvectorCpp1/test.desc b/regression/systemc/BitvectorCpp1/test.desc
new file mode 100644
index 00000000000..91d9cf8b52e
--- /dev/null
+++ b/regression/systemc/BitvectorCpp1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/BitvectorCpp2/main.cpp b/regression/systemc/BitvectorCpp2/main.cpp
new file mode 100644
index 00000000000..0b8f423136b
--- /dev/null
+++ b/regression/systemc/BitvectorCpp2/main.cpp
@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main(int argc, char** argv)
+{
+  __CPROVER::signedbv<4> x(15);
+  __CPROVER::signedbv<4> y;
+  y = 13;
+  x[1] = 0; //TODO: currently not supported
+  assert(x == y);
+
+  return 0;
+}
diff --git a/regression/systemc/BitvectorCpp2/test.desc b/regression/systemc/BitvectorCpp2/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/BitvectorCpp2/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/BitvectorSc1/main.cpp b/regression/systemc/BitvectorSc1/main.cpp
new file mode 100644
index 00000000000..333c10801cf
--- /dev/null
+++ b/regression/systemc/BitvectorSc1/main.cpp
@@ -0,0 +1,48 @@
+#include <cassert>
+
+template <int W>
+class sc_uint {
+  public:
+    sc_uint(unsigned long v)
+    {
+      width = W;
+      val = v;
+    }
+
+  void test1();
+  void test2()
+  {
+    unsigned long a[W];
+    a[W-1] = W;
+  }
+
+  unsigned long to_uint()
+  {
+    return val;
+  }
+
+protected:
+  int width;
+//  unsigned long val;
+  __CPROVER::unsignedbv<W> val;
+
+};
+
+template<int W>
+void sc_uint<W>::test1()
+{
+  width = W;
+}
+
+
+int main(int argc, char** argv)
+{
+  sc_uint<10> x(2);
+  x.test1();
+  x.test2();
+
+  assert(x.to_uint() == 1);
+  assert(x.to_uint() == 2);
+
+  return 0;
+}
diff --git a/regression/systemc/BitvectorSc1/test.desc b/regression/systemc/BitvectorSc1/test.desc
new file mode 100644
index 00000000000..65a2556e7e0
--- /dev/null
+++ b/regression/systemc/BitvectorSc1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/systemc/BitvectorSc2/main.cpp b/regression/systemc/BitvectorSc2/main.cpp
new file mode 100644
index 00000000000..6ebf3fd5a8b
--- /dev/null
+++ b/regression/systemc/BitvectorSc2/main.cpp
@@ -0,0 +1,62 @@
+#include <cassert>
+
+template <int W>
+class sc_uint {
+  public:
+    sc_uint(unsigned long v)
+    {
+      val = v;
+    }
+
+  sc_uint<W> &operator=(const sc_uint &other)
+  {
+    val = other.val;
+    return *this;
+  }
+
+  bool operator==(const sc_uint &other)
+  {
+    return val == other.val;
+  }
+
+#if 0
+  sc_uint<W> operator+(const sc_uint &other)
+  {
+    return sc_uint(val + other.val);
+  }
+#endif
+
+  sc_uint<W> operator += (const sc_uint &other)
+  {
+    val += other.val;
+    return *this;
+  }
+
+#if 0
+  sc_uint<W> operator += (unsigned long v)
+  {
+    val += v;
+    return *this;
+  }
+#endif
+
+protected:
+  __CPROVER::unsignedbv<W> val;
+
+};
+
+
+int main(int argc, char** argv)
+{
+  sc_uint<10> x(1);
+  sc_uint<10> y(2);
+
+  sc_uint<10> z(0);
+  z += x;
+  z += y;
+
+  sc_uint<10> w(3);
+  assert(z == w);
+
+  return 0;
+}
diff --git a/regression/systemc/BitvectorSc2/test.desc b/regression/systemc/BitvectorSc2/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/BitvectorSc2/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/BitvectorSc3/main.cpp b/regression/systemc/BitvectorSc3/main.cpp
new file mode 100644
index 00000000000..adf425cb9c4
--- /dev/null
+++ b/regression/systemc/BitvectorSc3/main.cpp
@@ -0,0 +1,44 @@
+#include <cassert>
+#include "../systemc_util.cpp"
+#include "../sc_uint_base.cpp"
+#include "../sc_uint.h"
+
+//#define IO
+
+#ifdef IO
+#include <iostream>
+#include <bitset>
+#endif
+
+int main(int argc, char** argv)
+{
+  //TODO: declaration alone doesn't type-check
+  sc_uint<8> x(221); //11011101
+  sc_uint<4> y(5);  //0101
+  sc_uint<4> z(12);  //1100
+
+#ifdef IO
+  std::cout << "x = " << std::bitset<MAX_SIZE>(x.to_uint()) << std::endl;
+  std::cout << "x.length() = " << x.length() << std::endl;
+  std::cout << "y = " << std::bitset<MAX_SIZE>(y.to_uint()) << std::endl;
+  std::cout << "z = " << std::bitset<MAX_SIZE>(z.to_uint()) << std::endl;
+  std::cout << "x.range(4,1) = " << std::bitset<MAX_SIZE>(x.range(4,1).to_uint()) << std::endl;
+  std::cout << "x.range(4,1).length() = " << x.range(4,1).length() << std::endl;
+#endif
+
+  x.range(4,1) = y; //1110 replaced by 0101
+  y = x.range(7,4); //1100
+
+#ifdef IO
+  std::cout << "x = " << std::bitset<MAX_SIZE>(x.to_uint()) << std::endl;
+  std::cout << "x.range(4,1) = " << std::bitset<MAX_SIZE>(x.range(4,1).to_uint()) << std::endl;
+  std::cout << "x.range(4,1).length() = " << x.range(4,1).length() << std::endl;
+  std::cout << "x.range(7,4) = " << std::bitset<MAX_SIZE>(x.range(7,4).to_uint()) << std::endl;
+  std::cout << "x.range(7,4).length() = " << x.range(7,4).length() << std::endl;
+  std::cout << "y = " << std::bitset<MAX_SIZE>(y.to_uint()) << std::endl;
+#endif
+
+  assert(y == z);
+
+  return 0;
+}
diff --git a/regression/systemc/BitvectorSc3/test.desc b/regression/systemc/BitvectorSc3/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/BitvectorSc3/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/CMakeLists.txt b/regression/systemc/CMakeLists.txt
new file mode 100644
index 00000000000..93d5ee716c2
--- /dev/null
+++ b/regression/systemc/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/systemc/Cast1/main.cpp b/regression/systemc/Cast1/main.cpp
new file mode 100644
index 00000000000..39e31d2fe4f
--- /dev/null
+++ b/regression/systemc/Cast1/main.cpp
@@ -0,0 +1,34 @@
+#include <cassert>
+#include "../systemc_util.cpp"
+#include "../sc_uint_base.cpp"
+#include "../sc_uint.h"
+
+//#define IO
+
+#ifdef IO
+#include <iostream>
+#include <bitset>
+#endif
+
+int main(int argc, char *argv[])
+{
+  sc_uint<3> a(6), d(5);
+  sc_uint<1> b, c;
+
+  b = (sc_uint<1>)a.range(2,2);
+  c = (sc_uint_base)a.range(0,0);
+  a.range(0,0) = b;
+  a.range(1,1) = c;
+
+#ifdef IO
+  std::cout << "a: " << a.to_uint() << std::endl;
+  std::cout << "b: " << b.to_uint() << std::endl;
+  std::cout << "c: " << c.to_uint() << std::endl;
+  std::cout << "d: " << d.to_uint() << std::endl;
+#endif
+
+  assert(a == d);
+
+  return 0;
+}
+
diff --git a/regression/systemc/Cast1/test.desc b/regression/systemc/Cast1/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/Cast1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/EqualOp1/main.cpp b/regression/systemc/EqualOp1/main.cpp
new file mode 100644
index 00000000000..dc0ee0c536d
--- /dev/null
+++ b/regression/systemc/EqualOp1/main.cpp
@@ -0,0 +1,24 @@
+#include <cassert>
+
+template<class T>
+class myclass
+{
+public:
+  myclass(T _m) : m(_m) {}
+
+  myclass<T> operator= (myclass<T> e);
+
+protected:
+  T m;
+};
+
+template<class T>
+myclass<T> myclass<T>::operator= (myclass<T> e) { m = e.m; return *this; }
+
+int main(int argc, char** argv)
+{
+  myclass<int> x(0);
+  myclass<int> y(1);
+  x = y;
+  assert(x == y);
+}
diff --git a/regression/systemc/EqualOp1/test.desc b/regression/systemc/EqualOp1/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/EqualOp1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/EqualOp2/main.cpp b/regression/systemc/EqualOp2/main.cpp
new file mode 100644
index 00000000000..1f656bf858d
--- /dev/null
+++ b/regression/systemc/EqualOp2/main.cpp
@@ -0,0 +1,30 @@
+#include <cassert>
+
+template<class T>
+class myclass
+{
+public:
+  explicit myclass(T _m) : m(_m) {}
+
+  myclass<T> &operator+= (int z) { m = z+2; return *this; }
+
+// TODO: doesn't work
+//  myclass<T> operator= (const myclass<T> &e) { m = e.m+2; return *this; }
+
+  bool operator== (const myclass<T> &e) { return (m == e.m); }
+
+protected:
+  T m;
+};
+
+// TODO: doesn't work
+// template<class T> myclass<T> myclass<T>::operator= (const myclass<T> &e) { m = e.m+2; return *this; }
+
+int main(int argc, char** argv)
+{
+  myclass<int> x(0);
+  myclass<int> y(1);
+  //x = y;
+  x += 1;
+  assert(x == y);
+}
diff --git a/regression/systemc/EqualOp2/test.desc b/regression/systemc/EqualOp2/test.desc
new file mode 100644
index 00000000000..65a2556e7e0
--- /dev/null
+++ b/regression/systemc/EqualOp2/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/systemc/EqualOp3/main.cpp b/regression/systemc/EqualOp3/main.cpp
new file mode 100644
index 00000000000..e910b6f2b39
--- /dev/null
+++ b/regression/systemc/EqualOp3/main.cpp
@@ -0,0 +1,43 @@
+#include <cassert>
+
+template<class T>
+class myclass2;
+
+template<class T>
+class myclass
+{
+public:
+  myclass(T _m) : m(_m) {}
+
+// TODO: doesn't work
+//  myclass<T> &operator= (const myclass<T> &e) { m = e.m+2; return *this; }
+//  myclass<T> operator= (myclass2<T> e) { m = e.m+2; return *this; }
+//  bool operator== (myclass<T> e) { return (m == e.m); }
+
+  T m;
+};
+
+template<class T>
+class myclass2
+{
+public:
+  myclass2(T _m) : m(_m) {}
+
+  myclass2<T> operator= (myclass<T> e) { m = e.m+2; return *this; }
+
+// TODO: doesn't work
+//  myclass2<T> operator= (myclass2<T> e) { m = e.m+2; return *this; }
+
+  bool operator== (myclass<T> e) { return (m == e.m); }
+
+  T m;
+};
+
+int main(int argc, char** argv)
+{
+  myclass2<int> x(0);
+  myclass<int> y(1);
+  x = y;
+  assert(x == y);
+  return 0;
+}
diff --git a/regression/systemc/EqualOp3/test.desc b/regression/systemc/EqualOp3/test.desc
new file mode 100644
index 00000000000..65a2556e7e0
--- /dev/null
+++ b/regression/systemc/EqualOp3/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/systemc/ForwardDecl1/main.cpp b/regression/systemc/ForwardDecl1/main.cpp
new file mode 100644
index 00000000000..615dde110d4
--- /dev/null
+++ b/regression/systemc/ForwardDecl1/main.cpp
@@ -0,0 +1,74 @@
+#include <cassert>
+
+#define INSIDE
+
+class sc_uint_subref;
+
+class sc_uint_base
+{
+ friend class sc_uint_subref;
+
+ public:
+  sc_uint_base(unsigned long v)
+    : val(v)
+  {
+  }
+
+  sc_uint_subref range(int left, int right)
+#ifndef INSIDE
+  ;
+#else
+  {
+    return sc_uint_subref(this, left, right);
+  }
+#endif
+
+ protected:
+  unsigned long val;
+};
+
+class sc_uint_subref
+{
+ friend class sc_uint_base;
+
+ public:
+  sc_uint_subref() {}
+  sc_uint_subref(sc_uint_base *_ptr, int _left, int _right)
+    : left(_left), right(_right), ptr(_ptr)
+  {}
+
+  bool operator==(const sc_uint_base &other)
+  {
+    return ptr->val == other.val;
+  }
+
+  sc_uint_subref &operator=(const sc_uint_subref &other)
+  {
+    ptr = other.ptr;
+    left = other.left;
+    right = other.right;
+    return *this;
+  }
+
+ protected:
+  int left, right;
+  sc_uint_base *ptr;
+
+};
+
+#ifndef INSIDE
+sc_uint_subref sc_uint_base::range(int left, int right)
+{
+  return sc_uint_subref(this, left, right);
+}
+#endif
+
+int main(int argc, char** argv)
+{
+  sc_uint_base x(42);
+  sc_uint_subref y = x.range(0,5);
+
+  assert(y == x);
+
+  return 0;
+}
diff --git a/regression/systemc/ForwardDecl1/test.desc b/regression/systemc/ForwardDecl1/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/ForwardDecl1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/FunTempl1/main.cpp b/regression/systemc/FunTempl1/main.cpp
new file mode 100644
index 00000000000..fda3e04ed39
--- /dev/null
+++ b/regression/systemc/FunTempl1/main.cpp
@@ -0,0 +1,19 @@
+#include <cassert>
+
+template<class T>
+T inc(T x)
+{
+  return x+1;
+}
+
+
+int main(int argc, char** argv)
+{
+  int x = 1;
+  unsigned char y = 2;
+  x = inc<int>(x);
+  x = inc<int>(x);
+  y = inc<unsigned char>(y);
+
+  assert(x == y);
+}
diff --git a/regression/systemc/FunTempl1/test.desc b/regression/systemc/FunTempl1/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/FunTempl1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/Makefile b/regression/systemc/Makefile
new file mode 100644
index 00000000000..486a8c750f7
--- /dev/null
+++ b/regression/systemc/Makefile
@@ -0,0 +1,19 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/cbmc/cbmc
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/cbmc/cbmc
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
diff --git a/regression/systemc/Masc1/main.cpp b/regression/systemc/Masc1/main.cpp
new file mode 100644
index 00000000000..ba7b1076017
--- /dev/null
+++ b/regression/systemc/Masc1/main.cpp
@@ -0,0 +1,48 @@
+#if 1
+typedef unsigned uint;
+#endif
+
+#include "masc.h"
+#include <cassert>
+
+mv<int,char> init_mv()
+{
+  char z=1;
+  mv<int,char> m(0,z);
+  return m;
+}
+
+void test_mv()
+{
+  mv<int,char> m = init_mv();
+
+  int x;
+  char y;
+  m.assign(x,y);
+
+  assert(x==0);
+  assert(y==1);
+}
+
+#define SIZE 5
+
+array<SIZE,int> init_array()
+{
+  array<SIZE,int> a;
+  for(int i=0;i<SIZE;i++)
+    a.elt[i] = i*i;
+  return a;
+}
+
+void test_array()
+{
+  array<SIZE,int> a = init_array();
+  assert(a.elt[SIZE-1]==(SIZE-1)*(SIZE-1));
+}
+
+int main (int argc, char *argv[])
+{
+  test_mv();
+  test_array();
+  return 0;
+}
diff --git a/regression/systemc/Masc1/masc.h b/regression/systemc/Masc1/masc.h
new file mode 100644
index 00000000000..137bd5bf562
--- /dev/null
+++ b/regression/systemc/Masc1/masc.h
@@ -0,0 +1,38 @@
+#ifndef MASC_H
+#define MASC_H
+
+typedef unsigned uint;
+
+// ---------------------------------------------------------------------
+// Templates for passing & returning tuples and arrays
+
+template <class T1, class T2, class T3 = bool, class T4 = bool>
+class mv {
+    T1 first;
+    T2 second;
+    T3 third;
+    T4 fourth;
+  public:
+    mv(T1 x, T2 y) {first = x; second = y;}
+    mv(T1 x, T2 y, T3 z) {first = x; second = y; third = z;}
+    mv(T1 x, T2 y, T3 z, T4 w) {first = x; second = y; third = z; fourth = w;}
+    void assign(T1 &x, T2 &y) {x = first; y = second;}
+    void assign(T1 &x, T2 &y, T3 &z) {x = first; y = second; z = third;}
+    void assign(T1 &x, T2 &y, T3 &z, T4 &w) {x = first; y = second; z = third; w = fourth;}
+};
+
+template <uint m, class T>
+class array {
+  public:
+    T elt[m];
+};
+
+
+// Assert is sometimes a macro, which screws up our translation.
+// If we are using the MASC translator we want to prevent its expansion.
+#ifdef __MASC__
+#undef assert
+#endif
+
+#endif
+
diff --git a/regression/systemc/Masc1/test.desc b/regression/systemc/Masc1/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/Masc1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/MascInst1/main.cpp b/regression/systemc/MascInst1/main.cpp
new file mode 100644
index 00000000000..34ec143957d
--- /dev/null
+++ b/regression/systemc/MascInst1/main.cpp
@@ -0,0 +1,60 @@
+#include <cassert>
+
+typedef unsigned uint;
+
+class mv_int_char {
+    int first;
+    char second;
+  public:
+    mv_int_char(int x, char y) {first = x; second = y;}
+    void assign(int &x, char &y) {x = first; y = second;}
+};
+
+class array_5_int {
+  public:
+    int elt[5];
+};
+
+mv_int_char init_mv()
+{
+  char z=1;
+  mv_int_char m(0,z);
+  return m;
+}
+
+void test_mv()
+{
+// TODO: doesn't work
+//  char z=1;
+//  mv_int_char m(0,z);
+
+   mv_int_char m = init_mv();
+
+  int x;
+  char y;
+  m.assign(x,y);
+
+  assert(x==0);
+  assert(y==1);
+}
+
+array_5_int init_array()
+{
+  array_5_int a;
+  for(int i=0;i<5;i++)
+    a.elt[i] = i*i;
+  return a;
+}
+
+void test_array()
+{
+  array_5_int a = init_array();
+  assert(a.elt[4]==16);
+}
+
+int main (int argc, char *argv[])
+{
+  test_mv();
+  test_array();
+  return 0;
+}
diff --git a/regression/systemc/MascInst1/masc.h b/regression/systemc/MascInst1/masc.h
new file mode 100644
index 00000000000..137bd5bf562
--- /dev/null
+++ b/regression/systemc/MascInst1/masc.h
@@ -0,0 +1,38 @@
+#ifndef MASC_H
+#define MASC_H
+
+typedef unsigned uint;
+
+// ---------------------------------------------------------------------
+// Templates for passing & returning tuples and arrays
+
+template <class T1, class T2, class T3 = bool, class T4 = bool>
+class mv {
+    T1 first;
+    T2 second;
+    T3 third;
+    T4 fourth;
+  public:
+    mv(T1 x, T2 y) {first = x; second = y;}
+    mv(T1 x, T2 y, T3 z) {first = x; second = y; third = z;}
+    mv(T1 x, T2 y, T3 z, T4 w) {first = x; second = y; third = z; fourth = w;}
+    void assign(T1 &x, T2 &y) {x = first; y = second;}
+    void assign(T1 &x, T2 &y, T3 &z) {x = first; y = second; z = third;}
+    void assign(T1 &x, T2 &y, T3 &z, T4 &w) {x = first; y = second; z = third; w = fourth;}
+};
+
+template <uint m, class T>
+class array {
+  public:
+    T elt[m];
+};
+
+
+// Assert is sometimes a macro, which screws up our translation.
+// If we are using the MASC translator we want to prevent its expansion.
+#ifdef __MASC__
+#undef assert
+#endif
+
+#endif
+
diff --git a/regression/systemc/MascInst1/test.desc b/regression/systemc/MascInst1/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/MascInst1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/Mult1/main.cpp b/regression/systemc/Mult1/main.cpp
new file mode 100644
index 00000000000..a89d76a1754
--- /dev/null
+++ b/regression/systemc/Mult1/main.cpp
@@ -0,0 +1,90 @@
+#include <cassert>
+#include "../systemc_util.cpp"
+#include "../sc_uint_base.cpp"
+#include "../sc_uint.h"
+
+//#define IO
+
+#define K 4 //8
+#define W 8 //32
+
+#ifdef IO
+#include <iostream>
+#include <bitset>
+#endif
+
+typedef unsigned int uint;
+typedef sc_uint<2*W+3> uint67_t;
+typedef sc_uint<K*W> uint256_t;
+typedef sc_uint<2*K*W> uint512_t;
+
+uint512_t mult256_impl (uint256_t a, uint256_t b)
+{
+#ifdef IO
+  std::cout << "a: " << a.to_uint() << std::endl;
+  std::cout << "b: " << b.to_uint() << std::endl;
+#endif
+  //TODO: implicit conversions
+  uint67_t p_product(0);  // = 0;
+  uint512_t result(0); // = 0;
+
+  uint i, k;
+
+  /* Compute each 32-bit "digit" of p_result, propagating the carries. */
+  for(k=0; k < 2*K-1; k++)
+  {
+    uint l_min = (k < K ? 0 : k-(K-1));
+#ifdef IO
+    std::cout << "k: " << k << std::endl;
+    std::cout << "l_min: " << l_min << std::endl;
+#endif
+    for(i=l_min; i<=k && i<K; i++)
+    {
+      p_product += (uint67_t)a.range(W*i+W-1,W*i) * b.range(W*(k-i)+W-1,W*(k-i));
+#ifdef IO
+      std::cout << "i: " << i << std::endl;
+      std::cout << "p_product: " << p_product.to_uint() << std::endl;
+#endif
+    }
+    result.range(k*W+W-1,k*W) = p_product.range(W-1,0); //.to_uint();
+#if 0
+    std::cout << "result.range(" << (k*W+W-1) << "," << (k*W) << "): " << result.range(k*W+W-1,k*W).to_uint() << std::endl;
+    std::cout << "p_product.range(" << (W-1) << ",0): " << p_product.range(W-1,0).to_uint() << std::endl;
+#endif
+    p_product >>= W;
+#ifdef IO
+    std::cout << "result: " << result.to_uint() << std::endl;
+    std::cout << "p_product: " << p_product.to_uint() << std::endl;
+#endif
+  }
+
+  result.range(k*W+W-1,k*W) = p_product.range(W-1,0); //.to_uint();
+#ifdef IO
+    std::cout << "result: " << result.to_uint() << std::endl;
+#endif
+  return result;
+}
+
+uint512_t bigmult (uint256_t a, uint256_t b) {
+  uint512_t result = a * b;
+  return result;
+}
+
+int main(int argc, char *argv[])
+{
+  uint256_t a(65535), b(65535);
+  uint512_t spec_r, impl_r;
+
+  spec_r = bigmult(a,b);
+  impl_r = mult256_impl(a,b);
+
+#ifdef IO
+  std::cout << "spec_r: " << spec_r.to_uint() << std::endl;
+  std::cout << "impl_r: " << impl_r.to_uint() << std::endl;
+#endif
+
+  assert(spec_r == impl_r);
+
+  return 0;
+}
+
diff --git a/regression/systemc/Mult1/test.desc b/regression/systemc/Mult1/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/Mult1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/Reference1/main.cpp b/regression/systemc/Reference1/main.cpp
new file mode 100644
index 00000000000..00c506da6da
--- /dev/null
+++ b/regression/systemc/Reference1/main.cpp
@@ -0,0 +1,23 @@
+#include <cassert>
+
+void test_ref(int &x)
+{
+  x = 2;
+}
+
+void test_ptr(int *x)
+{
+  *x = 3;
+}
+
+int main (int argc, char *argv[])
+{
+  int x = 0;
+  test_ref(x);
+  assert(x==2);
+
+  test_ptr(&x);
+  assert(x==3);
+
+  return 0;
+}
diff --git a/regression/systemc/Reference1/test.desc b/regression/systemc/Reference1/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/Reference1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/SimpleSc1/main.cpp b/regression/systemc/SimpleSc1/main.cpp
new file mode 100644
index 00000000000..379beb106ec
--- /dev/null
+++ b/regression/systemc/SimpleSc1/main.cpp
@@ -0,0 +1,60 @@
+#include <cassert>
+
+template <int W>
+class sc_uint {
+  public:
+    sc_uint(unsigned long v)
+    {
+      m_val = v;
+    }
+
+  sc_uint<W> &operator=(const sc_uint &other)
+  {
+    m_val = other.m_val;
+    return *this;
+  }
+
+  bool operator==(const sc_uint &other)
+  {
+    return m_val == other.m_val;
+  }
+
+#if 0
+  sc_uint<W> operator+(const sc_uint &other)
+  {
+    return sc_uint(m_val + other.m_val);
+  }
+#endif
+
+  sc_uint<W> operator += (const sc_uint &other)
+  {
+    m_val += other.m_val;
+    return *this;
+  }
+
+  sc_uint<W> operator += (unsigned long v)
+  {
+    m_val += v;
+    return *this;
+  }
+
+protected:
+  unsigned long m_val;
+};
+
+
+int main(int argc, char** argv)
+{
+  sc_uint<10> x(1);
+  sc_uint<10> y(2);
+
+//  sc_uint<10> z = x+y;
+  sc_uint<10> z(0);
+  z += x;
+  z += y;
+
+  sc_uint<10> w(3);
+  assert(z == w);
+
+  return 0;
+}
diff --git a/regression/systemc/SimpleSc1/test.desc b/regression/systemc/SimpleSc1/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/SimpleSc1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/Template1/main.cpp b/regression/systemc/Template1/main.cpp
new file mode 100644
index 00000000000..5702637542f
--- /dev/null
+++ b/regression/systemc/Template1/main.cpp
@@ -0,0 +1,42 @@
+#include <cassert>
+
+#define DEF_INSIDE
+
+template<class T>
+class my_template {
+  T m;
+public:
+  my_template() : m(0) {}
+  my_template(T _m) : m(_m) {}
+
+// TODO: doesn't work
+//  my_template(T _m) { m = _m; }
+
+  void set(T _m) { m = _m; }
+#ifdef DEF_INSIDE
+  T get() { return m; }
+#else
+  T get();
+#endif
+};
+
+#ifndef DEF_INSIDE
+template<class T>
+T my_template<T>::get()
+{
+  return m;
+}
+#endif
+
+
+int main (int argc, char *argv[])
+{
+  my_template<unsigned char> z(3);
+  my_template<int> x;
+  x.set(5);
+  int y = x.get();
+  assert(y==5);
+  assert(z.get()==3);
+
+  return 0;
+}
diff --git a/regression/systemc/Template1/test.desc b/regression/systemc/Template1/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/Template1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/This1/main.cpp b/regression/systemc/This1/main.cpp
new file mode 100644
index 00000000000..d6a9a7a21e2
--- /dev/null
+++ b/regression/systemc/This1/main.cpp
@@ -0,0 +1,37 @@
+#include <assert.h>
+
+class Foo;
+
+class Bar
+{
+public:
+  Bar(Foo* fp) : fooptr(fp) {}
+  //inline
+  void Set(int);
+  Foo* fooptr;
+};
+
+class Foo
+{
+public:
+  //inline
+  Bar bar() {
+    return Bar(this);
+  }
+  int value;
+};
+
+//inline
+void Bar::Set(int new_value)
+{
+  fooptr->value = new_value;
+}
+
+int main(void)
+{
+  Foo x;
+  x.bar().Set(42);
+  assert(x.value == 42);
+  x.bar().Set(99);
+  assert(x.value == 99);
+}
diff --git a/regression/systemc/This1/test.desc b/regression/systemc/This1/test.desc
new file mode 100644
index 00000000000..6666d172f47
--- /dev/null
+++ b/regression/systemc/This1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/Tuple1/main.cpp b/regression/systemc/Tuple1/main.cpp
new file mode 100644
index 00000000000..1784af494a9
--- /dev/null
+++ b/regression/systemc/Tuple1/main.cpp
@@ -0,0 +1,47 @@
+#include <cassert>
+#include "tuple.h"
+
+#ifndef NO_STRING
+#include <string>
+#endif
+
+int main(int argc, char** argv)
+{
+  tuple<int,int> p;
+  int x=0, y=0;
+
+  p = tuple<int,int>(1,2);
+
+#ifndef NO_IO
+  std::cout << p << std::endl;
+#endif
+
+  p = tuple<int,int>(3,4);
+
+#ifndef NO_IO
+  std::cout << p << std::endl;
+
+  std::cout << x << "," << y << std::endl;
+#endif
+  assert(x==0);
+  assert(y==0);
+
+  tie(x,y) = p;
+
+#ifndef NO_IO
+  std::cout << x << "," << y << std::endl;
+#endif
+  assert(x==3);
+  assert(y==4);
+
+  p = tuple<int,int>(5,6);
+
+#ifndef NO_IO
+  std::cout << p << std::endl;
+
+  std::cout << x << "," << y << std::endl;
+#endif
+  assert(x==3);
+  assert(y==4);
+
+}
diff --git a/regression/systemc/Tuple1/test.desc b/regression/systemc/Tuple1/test.desc
new file mode 100644
index 00000000000..839148c295a
--- /dev/null
+++ b/regression/systemc/Tuple1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+-DNO_IO -DNO_STRING
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/Tuple1/tuple.h b/regression/systemc/Tuple1/tuple.h
new file mode 100644
index 00000000000..388ae0020f7
--- /dev/null
+++ b/regression/systemc/Tuple1/tuple.h
@@ -0,0 +1,171 @@
+
+#ifndef TUPLE_H
+#define TUPLE_H
+
+#define DECLARE_INSIDE
+
+#ifndef NO_IO
+#include <iostream>
+#endif
+
+// ---------------------------------------------------------------------
+// Templates for passing & returning tuples
+
+// null type
+struct null_type {};
+
+// a const value of null_type
+inline const null_type cnull() {return null_type();}
+
+#ifndef NO_IO
+std::ostream& operator<<(std::ostream& os, const null_type dummy)
+{
+  os << "-";
+  return os;
+}
+#endif
+
+// a global to absorb "writes" to unused tuple fields.
+// would be good to get rid of this.
+null_type dummy;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class ltuple;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class tuple
+{
+
+  T0 el0;
+  T1 el1;
+  T2 el2;
+  T3 el3;
+
+public:
+
+  friend tuple<T0,T1,T2,T3>
+  ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3>);
+
+#ifndef NO_IO
+  std::ostream&
+  dump (std::ostream& os) {
+    os << "(" << el0 << "," << el1 << "," << el2 << "," << el3 << ")";
+    return os;
+  }
+#endif
+
+  tuple() {}
+
+  tuple(T0 t0): el0(t0), el1(cnull()), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1): el0(t0), el1(t1), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2): el0(t0), el1(t1), el2(t2), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2, T3 t3): el0(t0), el1(t1), el2(t2), el3(t3) {}
+
+};
+
+#ifndef NO_IO
+template<class T0, class T1, class T2, class T3>
+  std::ostream& operator<<(std::ostream& os, tuple<T0,T1,T2,T3> src)
+{
+  return src.dump(os);
+}
+#endif
+
+template
+   <class T0,
+    class T1,
+    class T2,
+    class T3>
+class ltuple
+{
+
+private:
+  T0 &el0;
+  T1 &el1;
+  T2 &el2;
+  T3 &el3;
+
+public:
+
+#ifdef DECLARE_INSIDE
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+    : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src)
+    {
+      el0 = src.el0;
+      el1 = src.el1;
+      el2 = src.el2;
+      el3 = src.el3;
+      return src;
+    }
+#else
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 );
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src);
+#endif
+};
+
+
+#ifndef DECLARE_INSIDE
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>::ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+  : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+template <class T0, class T1, class T2, class T3>
+tuple<T0,T1,T2,T3>
+ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3> src)
+{
+  el0 = src.el0;
+  el1 = src.el1;
+  el2 = src.el2;
+  el3 = src.el3;
+  return src;
+}
+#endif
+
+template <class T0>
+ltuple<T0>
+tie(T0 &t0)
+{
+  return ltuple<T0>(t0, dummy, dummy, dummy);
+}
+
+template <class T0, class T1>
+ltuple<T0,T1>
+tie(T0 &t0, T1 &t1)
+{
+  return ltuple<T0,T1>(t0,t1,dummy,dummy);
+}
+
+template <class T0, class T1, class T2>
+ltuple<T0,T1,T2>
+tie(T0 &t0, T1 &t1, T2 &t2)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,dummy);
+}
+
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>
+tie(T0 &t0, T1 &t1, T2 &t2, T3 &t3)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,t3);
+}
+
+#endif
+
diff --git a/regression/systemc/Tuple2/main.cpp b/regression/systemc/Tuple2/main.cpp
new file mode 100644
index 00000000000..3cb60834b4f
--- /dev/null
+++ b/regression/systemc/Tuple2/main.cpp
@@ -0,0 +1,120 @@
+#include <cassert>
+#include "tuple.h"
+
+#ifndef NO_STRING
+#include <string>
+#endif
+
+int main(int argc, char** argv)
+{
+  tuple<int,int> p;
+  int x=0, y=0;
+
+  p = tuple<int,int>(1,2);
+
+#ifndef NO_IO
+  std::cout << p << std::endl;
+#endif
+
+  p = tuple<int,int>(3,4);
+
+#ifndef NO_IO
+  std::cout << p << std::endl;
+
+  std::cout << x << "," << y << std::endl;
+#endif
+  assert(x==0);
+  assert(y==0);
+
+  tie(x,y) = p;
+
+#ifndef NO_IO
+  std::cout << x << "," << y << std::endl;
+#endif
+  assert(x==3);
+  assert(y==4);
+
+  p = tuple<int,int>(5,6);
+
+#ifndef NO_IO
+  std::cout << p << std::endl;
+
+  std::cout << x << "," << y << std::endl;
+#endif
+  assert(x==3);
+  assert(y==4);
+
+  x = 42; y = 69;
+
+#ifndef NO_IO
+  std::cout << p << std::endl;
+
+  std::cout << x << "," << y << std::endl;
+#endif
+  assert(x==42);
+  assert(y==69);
+
+  tuple<bool,bool> q;
+  q = tuple<bool,bool>(true,false);
+
+#ifndef NO_IO
+  std::cout << q << std::endl;
+#endif
+
+  bool foo, bar;
+
+  tie(foo,bar) = q;
+
+#ifndef NO_IO
+  std::cout << foo << " " << bar << std::endl;
+#endif
+  assert(foo);
+  assert(!bar);
+
+  tuple<int> one;
+  one = 69;
+
+#ifndef NO_IO
+  std::cout << one << std::endl;
+#endif
+
+  tie(x) = one;
+
+#ifndef NO_IO
+  std::cout << x << std::endl;
+#endif
+  assert(x==69);
+
+#ifndef NO_STRING
+  tuple<int,std::string,int> three;
+  three =   tuple<int,std::string,int>(42," does not equal ",69);
+
+#ifndef NO_IO
+  std::cout << three << std::endl;
+#endif
+
+  tuple<std::string,int,std::string,int> four;
+  four =   tuple<std::string,int,std::string,int>("and ", 42," is less than ",69);
+
+#ifndef NO_IO
+  std::cout << four << std::endl;
+#endif
+
+  tuple<std::string,std::string> msg;
+  msg = tuple<std::string,std::string>("hello","world");
+
+#ifndef NO_IO
+  std::cout << msg << std::endl;
+#endif
+
+  std::string xx,yy;
+  tie(xx,yy) = tuple<std::string,std::string>("hello","world");
+
+#ifndef NO_IO
+  std::cout << xx << " " << yy << std::endl;
+#endif
+  assert(xx=="hello");
+  assert(yy=="world");
+#endif
+
+}
diff --git a/regression/systemc/Tuple2/test.desc b/regression/systemc/Tuple2/test.desc
new file mode 100644
index 00000000000..839148c295a
--- /dev/null
+++ b/regression/systemc/Tuple2/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.cpp
+-DNO_IO -DNO_STRING
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/systemc/Tuple2/tuple.h b/regression/systemc/Tuple2/tuple.h
new file mode 100644
index 00000000000..388ae0020f7
--- /dev/null
+++ b/regression/systemc/Tuple2/tuple.h
@@ -0,0 +1,171 @@
+
+#ifndef TUPLE_H
+#define TUPLE_H
+
+#define DECLARE_INSIDE
+
+#ifndef NO_IO
+#include <iostream>
+#endif
+
+// ---------------------------------------------------------------------
+// Templates for passing & returning tuples
+
+// null type
+struct null_type {};
+
+// a const value of null_type
+inline const null_type cnull() {return null_type();}
+
+#ifndef NO_IO
+std::ostream& operator<<(std::ostream& os, const null_type dummy)
+{
+  os << "-";
+  return os;
+}
+#endif
+
+// a global to absorb "writes" to unused tuple fields.
+// would be good to get rid of this.
+null_type dummy;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class ltuple;
+
+template
+   <class T0 = null_type,
+    class T1 = null_type,
+    class T2 = null_type,
+    class T3 = null_type>
+class tuple
+{
+
+  T0 el0;
+  T1 el1;
+  T2 el2;
+  T3 el3;
+
+public:
+
+  friend tuple<T0,T1,T2,T3>
+  ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3>);
+
+#ifndef NO_IO
+  std::ostream&
+  dump (std::ostream& os) {
+    os << "(" << el0 << "," << el1 << "," << el2 << "," << el3 << ")";
+    return os;
+  }
+#endif
+
+  tuple() {}
+
+  tuple(T0 t0): el0(t0), el1(cnull()), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1): el0(t0), el1(t1), el2(cnull()), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2): el0(t0), el1(t1), el2(t2), el3(cnull()) {}
+
+  tuple(T0 t0, T1 t1, T2 t2, T3 t3): el0(t0), el1(t1), el2(t2), el3(t3) {}
+
+};
+
+#ifndef NO_IO
+template<class T0, class T1, class T2, class T3>
+  std::ostream& operator<<(std::ostream& os, tuple<T0,T1,T2,T3> src)
+{
+  return src.dump(os);
+}
+#endif
+
+template
+   <class T0,
+    class T1,
+    class T2,
+    class T3>
+class ltuple
+{
+
+private:
+  T0 &el0;
+  T1 &el1;
+  T2 &el2;
+  T3 &el3;
+
+public:
+
+#ifdef DECLARE_INSIDE
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+    : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src)
+    {
+      el0 = src.el0;
+      el1 = src.el1;
+      el2 = src.el2;
+      el3 = src.el3;
+      return src;
+    }
+#else
+  ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 );
+
+  tuple<T0,T1,T2,T3>
+  operator= (tuple<T0,T1,T2,T3> src);
+#endif
+};
+
+
+#ifndef DECLARE_INSIDE
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>::ltuple(T0 &t0, T1 &t1, T2 &t2, T3 &t3 )
+  : el0(t0), el1(t1), el2(t2), el3(t3)
+  {}
+
+template <class T0, class T1, class T2, class T3>
+tuple<T0,T1,T2,T3>
+ltuple<T0,T1,T2,T3>::operator= (tuple<T0,T1,T2,T3> src)
+{
+  el0 = src.el0;
+  el1 = src.el1;
+  el2 = src.el2;
+  el3 = src.el3;
+  return src;
+}
+#endif
+
+template <class T0>
+ltuple<T0>
+tie(T0 &t0)
+{
+  return ltuple<T0>(t0, dummy, dummy, dummy);
+}
+
+template <class T0, class T1>
+ltuple<T0,T1>
+tie(T0 &t0, T1 &t1)
+{
+  return ltuple<T0,T1>(t0,t1,dummy,dummy);
+}
+
+template <class T0, class T1, class T2>
+ltuple<T0,T1,T2>
+tie(T0 &t0, T1 &t1, T2 &t2)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,dummy);
+}
+
+template <class T0, class T1, class T2, class T3>
+ltuple<T0,T1,T2,T3>
+tie(T0 &t0, T1 &t1, T2 &t2, T3 &t3)
+{
+  return ltuple<T0,T1,T2>(t0,t1,t2,t3);
+}
+
+#endif
+
diff --git a/regression/systemc/sc_uint.h b/regression/systemc/sc_uint.h
new file mode 100644
index 00000000000..609b9cca2e3
--- /dev/null
+++ b/regression/systemc/sc_uint.h
@@ -0,0 +1,73 @@
+#ifndef SYSTEMC_SC_UINT_H
+#define SYSTEMC_SC_UINT_H
+
+#include <cassert>
+#include "sc_uint_base.h"
+
+template <int W>
+class sc_uint : public sc_uint_base
+{
+ public:
+  sc_uint() : sc_uint_base(0, W) {}
+
+  sc_uint(unsigned long v)
+    : sc_uint_base(v, W)
+  {
+  }
+
+  sc_uint(const sc_uint_base &b)
+    : sc_uint_base(b.val, W)
+  {
+  }
+
+  sc_uint(const sc_uint_subref &b)
+    : sc_uint_base(b)
+  {
+  }
+
+  sc_uint<W> &operator=(const sc_uint_base &other)
+  {
+    sc_uint_base::operator=(other);
+    return *this;
+  }
+
+  sc_uint<W> &operator=(const sc_uint_subref &other)
+  {
+    sc_uint_base::operator=(other);
+    return *this;
+  }
+
+  bool operator==(const sc_uint_base &other)
+  {
+    return sc_uint_base::operator==(other);
+  }
+
+  sc_uint<W> operator += (const sc_uint_base &other)
+  {
+    return sc_uint_base::operator+=(other);
+  }
+
+  sc_uint<W> operator *= (const sc_uint_base &other)
+  {
+    return sc_uint_base::operator*=(other);
+  }
+
+  sc_uint<W> operator+ (const sc_uint_base &other)
+  {
+    return sc_uint<W>(sc_uint_base::operator+(other));
+  }
+
+  sc_uint<W> operator* (const sc_uint_base &other)
+  {
+    return sc_uint<W>(sc_uint_base::operator*(other));
+  }
+
+  sc_uint<W> operator >>= (int v)
+  {
+    return sc_uint_base::operator>>=(v);
+  }
+
+};
+
+
+#endif
diff --git a/regression/systemc/sc_uint_base.cpp b/regression/systemc/sc_uint_base.cpp
new file mode 100644
index 00000000000..235eedd64f8
--- /dev/null
+++ b/regression/systemc/sc_uint_base.cpp
@@ -0,0 +1,42 @@
+#include <cassert>
+#include "sc_uint_base.h"
+
+sc_uint_base::sc_uint_base(const sc_uint_subref &other) :
+  val(0), m_len(other.length())
+{
+  bitvector_assign_from(other.ptr->val,other.right,other.length(),val);
+}
+
+sc_uint_base &sc_uint_base::operator=(const sc_uint_subref &other)
+{
+  bitvector_assign_from(other.ptr->val,other.right,other.length(),val);
+  return *this;
+}
+
+sc_uint_subref sc_uint_base::range(int left, int right)
+{
+  return sc_uint_subref(this, left, right);
+}
+
+//sc_uint_subref::operator sc_uint_base () { return sc_uint_base(*this); }
+
+sc_uint_base &sc_uint_subref::operator=(const sc_uint_base &other)
+{ 
+  bitvector_assign_to(other.val, ptr->val,right,other.length());
+  return *ptr;
+}
+
+sc_uint_base &sc_uint_subref::operator=(const sc_uint_subref &other)
+{ 
+  sc_uint_base tmp(0,length());
+  bitvector_assign_from(other.ptr->val,other.right,other.length(),tmp.val);
+  bitvector_assign_to(tmp.val, ptr->val,right,tmp.length());
+  return *ptr;
+}
+
+unsigned int sc_uint_subref::to_uint() const
+{
+  sc_uint_base tmp(0,length());
+  bitvector_assign_from(ptr->val,right,length(),tmp.val);
+  return tmp.to_uint();
+}
diff --git a/regression/systemc/sc_uint_base.h b/regression/systemc/sc_uint_base.h
new file mode 100644
index 00000000000..7fc7d8cb231
--- /dev/null
+++ b/regression/systemc/sc_uint_base.h
@@ -0,0 +1,114 @@
+#ifndef SYSTEMC_SC_UINT_BASE_H
+#define SYSTEMC_SC_UINT_BASE_H
+
+#include <cassert>
+#include "systemc_util.h"
+
+class sc_uint_subref;
+class sc_uint_base;
+
+class sc_uint_subref
+{
+ friend class sc_uint_base;
+ 
+ public:
+  sc_uint_subref(sc_uint_base *_ptr, int _left, int _right)
+    : ptr(_ptr), left(_left), right(_right)
+  {}
+
+  // TODO: doesn't work
+  // operator sc_uint_base ();
+
+  sc_uint_base &operator=(const sc_uint_base &other);
+  sc_uint_base &operator=(const sc_uint_subref &other);
+
+  int length() const
+  {
+    return left-right+1;
+  } 
+
+  unsigned int to_uint() const;
+
+ protected:
+  sc_uint_base *ptr;
+  int left, right;
+  
+};
+
+class sc_uint_base
+{
+ friend class sc_uint_subref;
+
+ public:
+  explicit sc_uint_base(unsigned long v, int _len)
+    : val(v), m_len(_len)
+  {
+  }
+
+  sc_uint_base(const sc_uint_subref &other);
+
+  sc_uint_base &operator=(const sc_uint_base &other)
+  {
+    val = other.val;
+    return *this;
+  }
+
+  sc_uint_base &operator=(const sc_uint_subref &other);
+  
+  bool operator==(const sc_uint_base &other)
+  {
+    return val == other.val;
+  }
+
+  sc_uint_base operator+=(const sc_uint_base &other)
+  {
+    val += other.val; 
+    return *this;
+  }
+
+  sc_uint_base operator-=(const sc_uint_base &other)
+  {
+    val -= other.val; 
+    return *this;
+  }
+
+  sc_uint_base operator*=(const sc_uint_base &other)
+  {
+    val *= other.val; 
+    return *this;
+  }
+
+  sc_uint_base operator>>=(int v) //uint_type v
+  {
+    val >>= v; 
+    return *this;
+  }
+
+  sc_uint_base operator+(const sc_uint_base &other)
+  {
+    return sc_uint_base(val+other.val, m_len);
+  }
+
+  sc_uint_base operator*(const sc_uint_base &other)
+  {
+    return sc_uint_base(val*other.val, m_len);
+  }
+
+  sc_uint_subref range(int left, int right);
+
+  int length() const
+  {
+    return m_len;
+  } 
+
+  unsigned int to_uint() const
+  {
+    return val;
+  }
+
+  bv_type val;
+ protected:
+  const int m_len;
+};
+
+#endif
diff --git a/regression/systemc/systemc_util.cpp b/regression/systemc/systemc_util.cpp
new file mode 100644
index 00000000000..98fb2e9d2fc
--- /dev/null
+++ b/regression/systemc/systemc_util.cpp
@@ -0,0 +1,33 @@
+#include "systemc_util.h"
+
+void bitvector_assign_to(
+  const bv_type &src,
+  bv_type &dst,
+  int offset,
+  int length)
+{
+  //TODO: we have to expose the bitvector_extract operator at the interface
+  bv_type tmpsrc = src;
+  tmpsrc <<= MAX_SIZE-length;
+  tmpsrc >>= MAX_SIZE-length;
+  tmpsrc <<= offset;
+  bv_type tmpdst1 = dst;
+  tmpdst1 >>= offset+length;
+  tmpdst1 <<= offset+length;
+  bv_type tmpdst2 = dst;
+  tmpdst2 <<= MAX_SIZE-offset;
+  tmpdst2 >>= MAX_SIZE-offset;
+  dst = tmpdst1 | tmpsrc | tmpdst2;
+}
+
+void bitvector_assign_from(
+  const bv_type &src,
+  int offset,
+  int length,
+  bv_type &dst)
+{
+  //TODO: we have to expose the bitvector_extract operator at the interface
+  dst = src;
+  dst <<= MAX_SIZE-(offset+length);
+  dst >>= MAX_SIZE-length;
+}
diff --git a/regression/systemc/systemc_util.h b/regression/systemc/systemc_util.h
new file mode 100644
index 00000000000..f8dece45942
--- /dev/null
+++ b/regression/systemc/systemc_util.h
@@ -0,0 +1,26 @@
+#ifndef SYSTEMC_UTIL_H
+#define SYSTEMC_UTIL_H
+
+//#define USE_BV
+
+#ifdef USE_BV
+#define MAX_SIZE 512
+typedef __CPROVER::unsignedbv<MAX_SIZE> bv_type;
+#else
+typedef unsigned long bv_type;
+#define MAX_SIZE (8*sizeof(bv_type))
+#endif
+
+void bitvector_assign_to(
+  const bv_type &src,
+  bv_type &dst,
+  int offset,
+  int length);
+
+void bitvector_assign_from(
+  const bv_type &src,
+  int offset,
+  int length,
+  bv_type &dst);
+
+#endif
diff --git a/scripts/cpplint.py b/scripts/cpplint.py
index b29a75205e4..7f72cf43df4 100755
--- a/scripts/cpplint.py
+++ b/scripts/cpplint.py
@@ -6536,7 +6536,7 @@ def ProcessFile(filename, vlevel, extra_check_functions=[]):
   if Search(r'_builtin_headers(_[a-z0-9_-]+)?\.h$', filename):
     return
 
-  if Search(r'regression/.*\.cpp', filename):
+  if Search(r'regression/.*\.(cpp|h)', filename):
     return
 
   if not ProcessConfigOverrides(filename):
diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp
index 252a9cb935e..419b5d1a382 100644
--- a/src/cpp/cpp_constructor.cpp
+++ b/src/cpp/cpp_constructor.cpp
@@ -41,7 +41,7 @@ codet cpp_typecheckt::cpp_constructor(
   {
     // We allow only one operand and it must be tagged with '#array_ini'.
     // Note that the operand is an array that is used for copy-initialization.
-    // In the general case, a program is not allow to use this form of
+    // In the general case, a program is not allowed to use this form of
     // construct. This way of initializing an array is used internally only.
     // The purpose of the tag #array_ini is to rule out ill-formed
     // programs.
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
index 8e3deb08872..fc1211a2d9d 100644
--- a/src/cpp/cpp_declarator_converter.cpp
+++ b/src/cpp/cpp_declarator_converter.cpp
@@ -44,7 +44,6 @@ symbolt &cpp_declarator_convertert::convert(
     typet type;
     type.swap(declarator.name().get_sub().back());
     declarator.type().subtype()=type;
-    std::string tmp;
     cpp_typecheck.typecheck_type(type);
     irept name(ID_name);
     name.set(ID_identifier, "("+cpp_type2name(type)+")");
diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp
index 44790ed2a42..896986cf869 100644
--- a/src/cpp/cpp_instantiate_template.cpp
+++ b/src/cpp/cpp_instantiate_template.cpp
@@ -238,7 +238,6 @@ const symbolt &cpp_typecheckt::instantiate_template(
   std::cout << "I: " << template_symbol.name << '\n';
   #endif
 
-  cpp_save_scopet cpp_saved_scope(cpp_scopes);
   cpp_saved_template_mapt saved_map(template_map);
 
   bool specialization_given=specialization.is_not_nil();
@@ -286,9 +285,6 @@ const symbolt &cpp_typecheckt::instantiate_template(
     throw 0;
   }
 
-  INVARIANT_STRUCTURED(
-    template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
-
   // produce new declaration
   cpp_declarationt new_decl=to_cpp_declaration(template_symbol.type);
 
@@ -417,7 +413,7 @@ const symbolt &cpp_typecheckt::instantiate_template(
 
     for(auto &tm : template_methods.operands())
     {
-      cpp_saved_scope.restore();
+      saved_scope.restore();
 
       cpp_declarationt method_decl=
         static_cast<const cpp_declarationt &>(
@@ -443,8 +439,7 @@ const symbolt &cpp_typecheckt::instantiate_template(
       convert(method_decl);
     }
 
-    const symbolt &new_symb=
-      lookup(new_decl.type().get(ID_identifier));
+    const symbolt &new_symb = lookup(new_decl.type().get(ID_identifier));
 
     return new_symb;
   }
diff --git a/src/cpp/cpp_scope.cpp b/src/cpp/cpp_scope.cpp
index 32d3f5a395f..502fab14e28 100644
--- a/src/cpp/cpp_scope.cpp
+++ b/src/cpp/cpp_scope.cpp
@@ -142,8 +142,8 @@ void cpp_scopet::lookup(
     other_scope.lookup(base_name, QUALIFIED, id_class, id_set);
   }
 
-  if(!id_set.empty() &&
-     id_class!=id_classt::TEMPLATE) return; // done, upwards scopes are hidden
+  if(!id_set.empty() && id_class != id_classt::TEMPLATE)
+    return; // done, upwards scopes are hidden
 
   // secondary scopes
   for(scope_listt::iterator
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index 1a749de3961..77a445777d8 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -884,7 +884,7 @@ void cpp_typecheckt::typecheck_friend_declaration(
 
   for(auto &sub_it : declaration.declarators())
   {
-    bool has_value=sub_it.value().is_not_nil();
+    bool has_value = sub_it.value().is_not_nil();
 
     if(!has_value)
     {
diff --git a/src/cpp/cpp_typecheck_method_bodies.cpp b/src/cpp/cpp_typecheck_method_bodies.cpp
index 5e134f79558..cbabd9e7728 100644
--- a/src/cpp/cpp_typecheck_method_bodies.cpp
+++ b/src/cpp/cpp_typecheck_method_bodies.cpp
@@ -30,11 +30,8 @@ void cpp_typecheckt::typecheck_method_bodies(
     if(body.id()=="cpp_not_typechecked")
       continue;
 
-    if(body.is_not_nil() &&
-       !body.is_zero())
-    {
+    if(body.is_not_nil() && !body.is_zero())
       convert_function(method_symbol);
-    }
   }
 
   old_instantiation_stack.swap(instantiation_stack);
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index c9b830be888..75659e72898 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -1041,8 +1041,6 @@ symbol_typet cpp_typecheck_resolvet::disambiguate_template_classes(
     throw 0;
   }
 
-  assert(primary_templates.size()==1);
-
   const symbolt &primary_template_symbol=
     cpp_typecheck.lookup(*primary_templates.begin());
 
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 648fd6b31df..91df5cb4447 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -1,4 +1,4 @@
-/**** ***************************************************************\
+/********************************************************************\
 
 Module: Goto Programs with Functions