3 files changed, 23 insertions, 23 deletions
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index f68465d1..39c9986a 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -10,7 +10,7 @@ procedure {:inline 1} Alloc() returns (x: Ref);
 
 
 
-implementation Alloc() returns (x: Ref)
+implementation {:inline 1} Alloc() returns (x: Ref)
 {
     assume $Alloc[x] == false && x != null;
     $Alloc[x] := true;
@@ -38,7 +38,7 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref);
 
 
 
-implementation System.Object.GetType(this: Ref) returns ($result: Ref)
+implementation {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
 {
     $result := $TypeOf($DynamicType(this));
 }
@@ -63,7 +63,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.Parameteriz
 
 
 
-implementation System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
 {
     assume $ThreadDelegate(this) == start$in;
 }
@@ -74,7 +74,7 @@ procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, par
 
 
 
-implementation System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+implementation {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
 {
     call {:async} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
 }
@@ -85,7 +85,7 @@ procedure {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$S
 
 
 
-implementation Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
+implementation {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
 {
     $Exception := null;
     call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in);
@@ -101,7 +101,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart
 
 
 
-implementation System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
+implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
 {
     assume $ThreadDelegate(this) == start$in;
 }
@@ -112,7 +112,7 @@ procedure {:inline 1} System.Threading.Thread.Start(this: Ref);
 
 
 
-implementation System.Threading.Thread.Start(this: Ref)
+implementation {:inline 1} System.Threading.Thread.Start(this: Ref)
 {
     call {:async} Wrapper_System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
 }
@@ -123,7 +123,7 @@ procedure {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref);
 
 
 
-implementation Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
+implementation {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
 {
     $Exception := null;
     call System.Threading.ThreadStart.Invoke(this);
@@ -159,7 +159,7 @@ procedure {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref);
 
 
 
-implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
+implementation {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
 {
   var d: Delegate;
 
@@ -184,7 +184,7 @@ procedure {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref);
 
 
 
-implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
+implementation {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
 {
   var d: Delegate;
 
@@ -213,7 +213,7 @@ procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref);
 
 
 
-implementation DelegateCreate(d: Delegate) returns (c: Ref)
+implementation {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref)
 {
     call c := Alloc();
     assume $Delegate(c) == MultisetSingleton(d);
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 9484ee38..22431543 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -8,7 +8,7 @@ procedure {:inline 1} Alloc() returns (x: Ref);
 
 
 
-implementation Alloc() returns (x: Ref)
+implementation {:inline 1} Alloc() returns (x: Ref)
 {
     assume $Alloc[x] == false && x != null;
     $Alloc[x] := true;
@@ -36,7 +36,7 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref);
 
 
 
-implementation System.Object.GetType(this: Ref) returns ($result: Ref)
+implementation {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
 {
     $result := $TypeOf($DynamicType(this));
 }
@@ -61,7 +61,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.Parameteriz
 
 
 
-implementation System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
 {
     assume $ThreadDelegate(this) == start$in;
 }
@@ -72,7 +72,7 @@ procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, par
 
 
 
-implementation System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+implementation {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
 {
     call {:async} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
 }
@@ -83,7 +83,7 @@ procedure {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$S
 
 
 
-implementation Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
+implementation {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
 {
     $Exception := null;
     call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in);
@@ -99,7 +99,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart
 
 
 
-implementation System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
+implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
 {
     assume $ThreadDelegate(this) == start$in;
 }
@@ -110,7 +110,7 @@ procedure {:inline 1} System.Threading.Thread.Start(this: Ref);
 
 
 
-implementation System.Threading.Thread.Start(this: Ref)
+implementation {:inline 1} System.Threading.Thread.Start(this: Ref)
 {
     call {:async} Wrapper_System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
 }
@@ -121,7 +121,7 @@ procedure {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref);
 
 
 
-implementation Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
+implementation {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
 {
     $Exception := null;
     call System.Threading.ThreadStart.Invoke(this);
@@ -157,7 +157,7 @@ procedure {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref);
 
 
 
-implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
+implementation {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
 {
   var d: Delegate;
 
@@ -182,7 +182,7 @@ procedure {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref);
 
 
 
-implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
+implementation {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
 {
   var d: Delegate;
 
@@ -211,7 +211,7 @@ procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref);
 
 
 
-implementation DelegateCreate(d: Delegate) returns (c: Ref)
+implementation {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref)
 {
     call c := Alloc();
     assume $Delegate(c) == MultisetSingleton(d);
diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index a8b5fdb2..a48be6af 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -61,7 +61,7 @@ namespace TranslationTest {
     #endregion
 
     private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {
-      BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, new Options(), null, false);
+      BCT.TranslateAssemblyAndWriteOutput(new List<string> { assemblyName }, heapFactory, new Options(), null, false);
       var fileName = Path.ChangeExtension(assemblyName, "bpl");
       var s = File.ReadAllText(fileName);
       return s;