dafny-lang · keyboardDrummer · Oct 18, 2023 · Oct 5, 2023 · Oct 5, 2023 · Oct 5, 2023
diff --git a/.gitmodules b/.gitmodules
@@ -1,3 +1,3 @@
 [submodule "Test/libraries"]
- path = Test/libraries
+ path = Source/IntegrationTests/TestFiles/LitTests/LitTest/libraries
  url = https://github.com/dafny-lang/libraries.git
diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj
@@ -127,10 +127,10 @@
  </ItemGroup>
 
  <ItemGroup>
- <None Include="..\..\Test\dafny3\GenericSort.dfy" Link="Various\TestFiles\GenericSort.dfy">
+ <None Include="..\IntegrationTests\TestFiles\LitTests\LitTest\dafny3\GenericSort.dfy" Link="Various\TestFiles\GenericSort.dfy">
  <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
  </None>
- <None Include="..\..\Test\dafny4\GHC-MergeSort.dfy" Link="Various\TestFiles\GHC-MergeSort.dfy">
+ <None Include="..\IntegrationTests\TestFiles\LitTests\LitTest\dafny4\GHC-MergeSort.dfy" Link="Various\TestFiles\GHC-MergeSort.dfy">
  <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
  </None>
  </ItemGroup>

diff --git a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj
@@ -34,7 +34,7 @@
  <Content Include="..\..\Binaries\z3\**\*.*" LinkBase="z3">
  <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
  </Content>
- <Content Include="..\..\Test\dafny0\warnings-as-errors.dfy">
+ <Content Include="..\IntegrationTests\TestFiles\LitTests\LitTest\dafny0\warnings-as-errors.dfy">
  <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
  </Content>
  </ItemGroup>

diff --git a/Source/IntegrationTests/IntegrationTests.csproj b/Source/IntegrationTests/IntegrationTests.csproj
@@ -5,6 +5,7 @@
  <GenerateEmbeddedFilesManifest>true</GenerateEmbeddedFilesManifest>
  <IsPackable>false</IsPackable>
  <Nullable>enable</Nullable>
+ <DefaultItemExcludes>$(DefaultItemExcludes);TestFiles\**\*.*</DefaultItemExcludes>
  </PropertyGroup>
 
  <ItemGroup>
@@ -39,7 +40,7 @@
  <Content Include="..\..\Binaries\z3\**\*.*" LinkBase="z3">
  <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
  </Content>
- <Content Include="..\..\Test\**\*.*" Exclude="..\..\Test\**\.#*" LinkBase="TestFiles\LitTests\LitTest">
+ <Content Include="TestFiles\LitTests\LitTest\**\*.*" Exclude="TestFiles\LitTests\LitTest\**\.#*">
  <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
  </Content>
  <Content Include="..\..\docs\DafnyRef\examples\**\*.*" LinkBase="TestFiles\LitTests\LitTest\refman\examples">

diff --git a/Test/.gitignore → ...sts/TestFiles/LitTests/LitTest/.gitignore b/Test/.gitignore → ...sts/TestFiles/LitTests/LitTest/.gitignore
diff --git a/Test/DafnyTests/DafnyTests.csproj → ...ests/LitTest/DafnyTests/DafnyTests.csproj b/Test/DafnyTests/DafnyTests.csproj → ...ests/LitTest/DafnyTests/DafnyTests.csproj
diff --git a/Test/DafnyTests/RunAllTestsOption.dfy → .../LitTest/DafnyTests/RunAllTestsOption.dfy b/Test/DafnyTests/RunAllTestsOption.dfy → .../LitTest/DafnyTests/RunAllTestsOption.dfy
diff --git a/Test/DafnyTests/RunAllTestsOption.dfy.expect → ...t/DafnyTests/RunAllTestsOption.dfy.expect b/Test/DafnyTests/RunAllTestsOption.dfy.expect → ...t/DafnyTests/RunAllTestsOption.dfy.expect
diff --git a/Test/DafnyTests/TestAttribute.dfy → ...ests/LitTest/DafnyTests/TestAttribute.dfy b/Test/DafnyTests/TestAttribute.dfy → ...ests/LitTest/DafnyTests/TestAttribute.dfy
diff --git a/Test/DafnyTests/zeroExitCodeTests.dfy → .../LitTest/DafnyTests/zeroExitCodeTests.dfy b/Test/DafnyTests/zeroExitCodeTests.dfy → .../LitTest/DafnyTests/zeroExitCodeTests.dfy
diff --git a/...Specification/ReadPreconditionBypass1.dfy → ...Specification/ReadPreconditionBypass1.dfy b/...Specification/ReadPreconditionBypass1.dfy → ...Specification/ReadPreconditionBypass1.dfy
diff --git a/...cation/ReadPreconditionBypass1.dfy.expect → ...cation/ReadPreconditionBypass1.dfy.expect b/...cation/ReadPreconditionBypass1.dfy.expect → ...cation/ReadPreconditionBypass1.dfy.expect
diff --git a/...Specification/ReadPreconditionBypass2.dfy → ...Specification/ReadPreconditionBypass2.dfy b/...Specification/ReadPreconditionBypass2.dfy → ...Specification/ReadPreconditionBypass2.dfy
diff --git a/...cation/ReadPreconditionBypass2.dfy.expect → ...cation/ReadPreconditionBypass2.dfy.expect b/...cation/ReadPreconditionBypass2.dfy.expect → ...cation/ReadPreconditionBypass2.dfy.expect
diff --git a/...Specification/ReadPreconditionBypass3.dfy → ...Specification/ReadPreconditionBypass3.dfy b/...Specification/ReadPreconditionBypass3.dfy → ...Specification/ReadPreconditionBypass3.dfy
diff --git a/...cation/ReadPreconditionBypass3.dfy.expect → ...cation/ReadPreconditionBypass3.dfy.expect b/...cation/ReadPreconditionBypass3.dfy.expect → ...cation/ReadPreconditionBypass3.dfy.expect
diff --git a/...Specification/ReadPreconditionBypass4.dfy → ...Specification/ReadPreconditionBypass4.dfy b/...Specification/ReadPreconditionBypass4.dfy → ...Specification/ReadPreconditionBypass4.dfy
diff --git a/...cation/ReadPreconditionBypass4.dfy.expect → ...cation/ReadPreconditionBypass4.dfy.expect b/...cation/ReadPreconditionBypass4.dfy.expect → ...cation/ReadPreconditionBypass4.dfy.expect
diff --git a/Test/Landin/Knot1.dfy → ...stFiles/LitTests/LitTest/Landin/Knot1.dfy b/Test/Landin/Knot1.dfy → ...stFiles/LitTests/LitTest/Landin/Knot1.dfy
diff --git a/Test/Landin/Knot1.dfy.expect → .../LitTests/LitTest/Landin/Knot1.dfy.expect b/Test/Landin/Knot1.dfy.expect → .../LitTests/LitTest/Landin/Knot1.dfy.expect
diff --git a/Test/Landin/Knot10.dfy → ...tFiles/LitTests/LitTest/Landin/Knot10.dfy b/Test/Landin/Knot10.dfy → ...tFiles/LitTests/LitTest/Landin/Knot10.dfy
diff --git a/Test/Landin/Knot10.dfy.expect → ...LitTests/LitTest/Landin/Knot10.dfy.expect b/Test/Landin/Knot10.dfy.expect → ...LitTests/LitTest/Landin/Knot10.dfy.expect
diff --git a/Test/Landin/Knot11.dfy → ...tFiles/LitTests/LitTest/Landin/Knot11.dfy b/Test/Landin/Knot11.dfy → ...tFiles/LitTests/LitTest/Landin/Knot11.dfy
diff --git a/Test/Landin/Knot11.dfy.expect → ...LitTests/LitTest/Landin/Knot11.dfy.expect b/Test/Landin/Knot11.dfy.expect → ...LitTests/LitTest/Landin/Knot11.dfy.expect
diff --git a/Test/Landin/Knot12.dfy → ...tFiles/LitTests/LitTest/Landin/Knot12.dfy b/Test/Landin/Knot12.dfy → ...tFiles/LitTests/LitTest/Landin/Knot12.dfy
diff --git a/Test/Landin/Knot12.dfy.expect → ...LitTests/LitTest/Landin/Knot12.dfy.expect b/Test/Landin/Knot12.dfy.expect → ...LitTests/LitTest/Landin/Knot12.dfy.expect
diff --git a/Test/Landin/Knot13.dfy → ...tFiles/LitTests/LitTest/Landin/Knot13.dfy b/Test/Landin/Knot13.dfy → ...tFiles/LitTests/LitTest/Landin/Knot13.dfy
diff --git a/Test/Landin/Knot13.dfy.expect → ...LitTests/LitTest/Landin/Knot13.dfy.expect b/Test/Landin/Knot13.dfy.expect → ...LitTests/LitTest/Landin/Knot13.dfy.expect
diff --git a/Test/Landin/Knot14.dfy → ...tFiles/LitTests/LitTest/Landin/Knot14.dfy b/Test/Landin/Knot14.dfy → ...tFiles/LitTests/LitTest/Landin/Knot14.dfy
diff --git a/Test/Landin/Knot14.dfy.expect → ...LitTests/LitTest/Landin/Knot14.dfy.expect b/Test/Landin/Knot14.dfy.expect → ...LitTests/LitTest/Landin/Knot14.dfy.expect
diff --git a/Test/Landin/Knot15.dfy → ...tFiles/LitTests/LitTest/Landin/Knot15.dfy b/Test/Landin/Knot15.dfy → ...tFiles/LitTests/LitTest/Landin/Knot15.dfy
diff --git a/Test/Landin/Knot15.dfy.expect → ...LitTests/LitTest/Landin/Knot15.dfy.expect b/Test/Landin/Knot15.dfy.expect → ...LitTests/LitTest/Landin/Knot15.dfy.expect
diff --git a/Test/Landin/Knot16.dfy → ...tFiles/LitTests/LitTest/Landin/Knot16.dfy b/Test/Landin/Knot16.dfy → ...tFiles/LitTests/LitTest/Landin/Knot16.dfy
diff --git a/Test/Landin/Knot16.dfy.expect → ...LitTests/LitTest/Landin/Knot16.dfy.expect b/Test/Landin/Knot16.dfy.expect → ...LitTests/LitTest/Landin/Knot16.dfy.expect
diff --git a/Test/Landin/Knot17.dfy → ...tFiles/LitTests/LitTest/Landin/Knot17.dfy b/Test/Landin/Knot17.dfy → ...tFiles/LitTests/LitTest/Landin/Knot17.dfy
diff --git a/Test/Landin/Knot17.dfy.expect → ...LitTests/LitTest/Landin/Knot17.dfy.expect b/Test/Landin/Knot17.dfy.expect → ...LitTests/LitTest/Landin/Knot17.dfy.expect
diff --git a/Test/Landin/Knot2.dfy → ...stFiles/LitTests/LitTest/Landin/Knot2.dfy b/Test/Landin/Knot2.dfy → ...stFiles/LitTests/LitTest/Landin/Knot2.dfy
diff --git a/Test/Landin/Knot2.dfy.expect → .../LitTests/LitTest/Landin/Knot2.dfy.expect b/Test/Landin/Knot2.dfy.expect → .../LitTests/LitTest/Landin/Knot2.dfy.expect
diff --git a/Test/Landin/Knot3.dfy → ...stFiles/LitTests/LitTest/Landin/Knot3.dfy b/Test/Landin/Knot3.dfy → ...stFiles/LitTests/LitTest/Landin/Knot3.dfy
diff --git a/Test/Landin/Knot3.dfy.expect → .../LitTests/LitTest/Landin/Knot3.dfy.expect b/Test/Landin/Knot3.dfy.expect → .../LitTests/LitTest/Landin/Knot3.dfy.expect
diff --git a/Test/Landin/Knot4.dfy → ...stFiles/LitTests/LitTest/Landin/Knot4.dfy b/Test/Landin/Knot4.dfy → ...stFiles/LitTests/LitTest/Landin/Knot4.dfy
diff --git a/Test/Landin/Knot4.dfy.expect → .../LitTests/LitTest/Landin/Knot4.dfy.expect b/Test/Landin/Knot4.dfy.expect → .../LitTests/LitTest/Landin/Knot4.dfy.expect
diff --git a/Test/Landin/Knot5.dfy → ...stFiles/LitTests/LitTest/Landin/Knot5.dfy b/Test/Landin/Knot5.dfy → ...stFiles/LitTests/LitTest/Landin/Knot5.dfy
diff --git a/Test/Landin/Knot5.dfy.expect → .../LitTests/LitTest/Landin/Knot5.dfy.expect b/Test/Landin/Knot5.dfy.expect → .../LitTests/LitTest/Landin/Knot5.dfy.expect
diff --git a/Test/Landin/Knot6.dfy → ...stFiles/LitTests/LitTest/Landin/Knot6.dfy b/Test/Landin/Knot6.dfy → ...stFiles/LitTests/LitTest/Landin/Knot6.dfy
diff --git a/Test/Landin/Knot6.dfy.expect → .../LitTests/LitTest/Landin/Knot6.dfy.expect b/Test/Landin/Knot6.dfy.expect → .../LitTests/LitTest/Landin/Knot6.dfy.expect
diff --git a/Test/Landin/Knot7.dfy → ...stFiles/LitTests/LitTest/Landin/Knot7.dfy b/Test/Landin/Knot7.dfy → ...stFiles/LitTests/LitTest/Landin/Knot7.dfy
diff --git a/Test/Landin/Knot7.dfy.expect → .../LitTests/LitTest/Landin/Knot7.dfy.expect b/Test/Landin/Knot7.dfy.expect → .../LitTests/LitTest/Landin/Knot7.dfy.expect
diff --git a/Test/Landin/Knot8.dfy → ...stFiles/LitTests/LitTest/Landin/Knot8.dfy b/Test/Landin/Knot8.dfy → ...stFiles/LitTests/LitTest/Landin/Knot8.dfy
diff --git a/Test/Landin/Knot8.dfy.expect → .../LitTests/LitTest/Landin/Knot8.dfy.expect b/Test/Landin/Knot8.dfy.expect → .../LitTests/LitTest/Landin/Knot8.dfy.expect
diff --git a/Test/Landin/Knot9.dfy → ...stFiles/LitTests/LitTest/Landin/Knot9.dfy b/Test/Landin/Knot9.dfy → ...stFiles/LitTests/LitTest/Landin/Knot9.dfy
diff --git a/Test/Landin/Knot9.dfy.expect → .../LitTests/LitTest/Landin/Knot9.dfy.expect b/Test/Landin/Knot9.dfy.expect → .../LitTests/LitTest/Landin/Knot9.dfy.expect
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md b/Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md
@@ -0,0 +1 @@
+The folder Test has been moved to Source/IntegrationTests/TestFiles/LitTests/LitTest
diff --git a/Test/VSComp2010/Problem1-SumMax.dfy → ...ts/LitTest/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy → ...ts/LitTest/VSComp2010/Problem1-SumMax.dfy
diff --git a/Test/VSComp2010/Problem1-SumMax.dfy.expect → ...est/VSComp2010/Problem1-SumMax.dfy.expect b/Test/VSComp2010/Problem1-SumMax.dfy.expect → ...est/VSComp2010/Problem1-SumMax.dfy.expect
diff --git a/Test/VSComp2010/Problem2-Invert.dfy → ...ts/LitTest/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy → ...ts/LitTest/VSComp2010/Problem2-Invert.dfy
diff --git a/Test/VSComp2010/Problem2-Invert.dfy.expect → ...est/VSComp2010/Problem2-Invert.dfy.expect b/Test/VSComp2010/Problem2-Invert.dfy.expect → ...est/VSComp2010/Problem2-Invert.dfy.expect
diff --git a/Test/VSComp2010/Problem3-FindZero.dfy → .../LitTest/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy → .../LitTest/VSComp2010/Problem3-FindZero.dfy
diff --git a/Test/VSComp2010/Problem3-FindZero.dfy.expect → ...t/VSComp2010/Problem3-FindZero.dfy.expect b/Test/VSComp2010/Problem3-FindZero.dfy.expect → ...t/VSComp2010/Problem3-FindZero.dfy.expect
diff --git a/Test/VSComp2010/Problem4-Queens.dfy → ...ts/LitTest/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy → ...ts/LitTest/VSComp2010/Problem4-Queens.dfy
diff --git a/Test/VSComp2010/Problem4-Queens.dfy.expect → ...est/VSComp2010/Problem4-Queens.dfy.expect b/Test/VSComp2010/Problem4-Queens.dfy.expect → ...est/VSComp2010/Problem4-Queens.dfy.expect
diff --git a/.../VSComp2010/Problem5-DoubleEndedQueue.dfy → .../VSComp2010/Problem5-DoubleEndedQueue.dfy b/.../VSComp2010/Problem5-DoubleEndedQueue.dfy → .../VSComp2010/Problem5-DoubleEndedQueue.dfy
diff --git a/...2010/Problem5-DoubleEndedQueue.dfy.expect → ...2010/Problem5-DoubleEndedQueue.dfy.expect b/...2010/Problem5-DoubleEndedQueue.dfy.expect → ...2010/Problem5-DoubleEndedQueue.dfy.expect
diff --git a/Test/VSI-Benchmarks/b1.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b1.dfy
diff --git a/Test/VSI-Benchmarks/b1.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b1.dfy.expect b/Test/VSI-Benchmarks/b1.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b1.dfy.expect
diff --git a/Test/VSI-Benchmarks/b2.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b2.dfy
diff --git a/Test/VSI-Benchmarks/b2.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b2.dfy.expect b/Test/VSI-Benchmarks/b2.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b2.dfy.expect
diff --git a/Test/VSI-Benchmarks/b3.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b3.dfy
diff --git a/Test/VSI-Benchmarks/b3.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b3.dfy.expect b/Test/VSI-Benchmarks/b3.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b3.dfy.expect
diff --git a/Test/VSI-Benchmarks/b4.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b4.dfy
diff --git a/Test/VSI-Benchmarks/b4.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b4.dfy.expect b/Test/VSI-Benchmarks/b4.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b4.dfy.expect
diff --git a/Test/VSI-Benchmarks/b5.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b5.dfy
diff --git a/Test/VSI-Benchmarks/b5.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b5.dfy.expect b/Test/VSI-Benchmarks/b5.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b5.dfy.expect
diff --git a/Test/VSI-Benchmarks/b6.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b6.dfy
diff --git a/Test/VSI-Benchmarks/b6.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b6.dfy.expect b/Test/VSI-Benchmarks/b6.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b6.dfy.expect
diff --git a/Test/VSI-Benchmarks/b7.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b7.dfy
diff --git a/Test/VSI-Benchmarks/b7.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b7.dfy.expect b/Test/VSI-Benchmarks/b7.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b7.dfy.expect
diff --git a/Test/VSI-Benchmarks/b8.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy → ...es/LitTests/LitTest/VSI-Benchmarks/b8.dfy
diff --git a/Test/VSI-Benchmarks/b8.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b8.dfy.expect b/Test/VSI-Benchmarks/b8.dfy.expect → ...ests/LitTest/VSI-Benchmarks/b8.dfy.expect
diff --git a/Test/VerifyThis2015/Problem1.dfy → ...Tests/LitTest/VerifyThis2015/Problem1.dfy b/Test/VerifyThis2015/Problem1.dfy → ...Tests/LitTest/VerifyThis2015/Problem1.dfy
diff --git a/Test/VerifyThis2015/Problem1.dfy.expect → ...itTest/VerifyThis2015/Problem1.dfy.expect b/Test/VerifyThis2015/Problem1.dfy.expect → ...itTest/VerifyThis2015/Problem1.dfy.expect
diff --git a/Test/VerifyThis2015/Problem2.dfy → ...Tests/LitTest/VerifyThis2015/Problem2.dfy b/Test/VerifyThis2015/Problem2.dfy → ...Tests/LitTest/VerifyThis2015/Problem2.dfy
diff --git a/Test/VerifyThis2015/Problem2.dfy.expect → ...itTest/VerifyThis2015/Problem2.dfy.expect b/Test/VerifyThis2015/Problem2.dfy.expect → ...itTest/VerifyThis2015/Problem2.dfy.expect
diff --git a/Test/VerifyThis2015/Problem3.dfy → ...Tests/LitTest/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy → ...Tests/LitTest/VerifyThis2015/Problem3.dfy
diff --git a/Test/VerifyThis2015/Problem3.dfy.expect → ...itTest/VerifyThis2015/Problem3.dfy.expect b/Test/VerifyThis2015/Problem3.dfy.expect → ...itTest/VerifyThis2015/Problem3.dfy.expect
diff --git a/Test/attr-help.dfy → .../TestFiles/LitTests/LitTest/attr-help.dfy b/Test/attr-help.dfy → .../TestFiles/LitTests/LitTest/attr-help.dfy
diff --git a/Test/auditor/IgnoredAssumptions.dfy → ...ts/LitTest/auditor/IgnoredAssumptions.dfy b/Test/auditor/IgnoredAssumptions.dfy → ...ts/LitTest/auditor/IgnoredAssumptions.dfy
diff --git a/Test/auditor/TestAuditor.dfy → .../LitTests/LitTest/auditor/TestAuditor.dfy b/Test/auditor/TestAuditor.dfy → .../LitTests/LitTest/auditor/TestAuditor.dfy
diff --git a/Test/auditor/TestAuditor.dfy-ietf.md.expect → ...st/auditor/TestAuditor.dfy-ietf.md.expect b/Test/auditor/TestAuditor.dfy-ietf.md.expect → ...st/auditor/TestAuditor.dfy-ietf.md.expect
diff --git a/Test/auditor/TestAuditor.dfy.expect → ...ts/LitTest/auditor/TestAuditor.dfy.expect b/Test/auditor/TestAuditor.dfy.expect → ...ts/LitTest/auditor/TestAuditor.dfy.expect
diff --git a/Test/auditor/TestAuditor.dfy.html.expect → ...tTest/auditor/TestAuditor.dfy.html.expect b/Test/auditor/TestAuditor.dfy.html.expect → ...tTest/auditor/TestAuditor.dfy.html.expect
diff --git a/Test/auditor/TestAuditor.dfy.md.expect → ...LitTest/auditor/TestAuditor.dfy.md.expect b/Test/auditor/TestAuditor.dfy.md.expect → ...LitTest/auditor/TestAuditor.dfy.md.expect
diff --git a/Test/autoRevealDependencies/ast.dfy → ...ts/LitTest/autoRevealDependencies/ast.dfy b/Test/autoRevealDependencies/ast.dfy → ...ts/LitTest/autoRevealDependencies/ast.dfy
diff --git a/Test/autoRevealDependencies/ast.dfy.expect → ...est/autoRevealDependencies/ast.dfy.expect b/Test/autoRevealDependencies/ast.dfy.expect → ...est/autoRevealDependencies/ast.dfy.expect
diff --git a/Test/autoRevealDependencies/complicated.dfy → ...st/autoRevealDependencies/complicated.dfy b/Test/autoRevealDependencies/complicated.dfy → ...st/autoRevealDependencies/complicated.dfy
diff --git a/...RevealDependencies/complicated.dfy.expect → ...RevealDependencies/complicated.dfy.expect b/...RevealDependencies/complicated.dfy.expect → ...RevealDependencies/complicated.dfy.expect
diff --git a/...toRevealDependencies/datatype-reveals.dfy → ...toRevealDependencies/datatype-reveals.dfy b/...toRevealDependencies/datatype-reveals.dfy → ...toRevealDependencies/datatype-reveals.dfy
diff --git a/...lDependencies/datatype-reveals.dfy.expect → ...lDependencies/datatype-reveals.dfy.expect b/...lDependencies/datatype-reveals.dfy.expect → ...lDependencies/datatype-reveals.dfy.expect
diff --git a/Test/autoRevealDependencies/dfyconfig.toml → ...est/autoRevealDependencies/dfyconfig.toml b/Test/autoRevealDependencies/dfyconfig.toml → ...est/autoRevealDependencies/dfyconfig.toml
diff --git a/...utoRevealDependencies/func-depth-fail.dfy → ...utoRevealDependencies/func-depth-fail.dfy b/...utoRevealDependencies/func-depth-fail.dfy → ...utoRevealDependencies/func-depth-fail.dfy
diff --git a/...alDependencies/func-depth-fail.dfy.expect → ...alDependencies/func-depth-fail.dfy.expect b/...alDependencies/func-depth-fail.dfy.expect → ...alDependencies/func-depth-fail.dfy.expect
diff --git a/...utoRevealDependencies/func-depth-succ.dfy → ...utoRevealDependencies/func-depth-succ.dfy b/...utoRevealDependencies/func-depth-succ.dfy → ...utoRevealDependencies/func-depth-succ.dfy
diff --git a/...alDependencies/func-depth-succ.dfy.expect → ...alDependencies/func-depth-succ.dfy.expect b/...alDependencies/func-depth-succ.dfy.expect → ...alDependencies/func-depth-succ.dfy.expect
diff --git a/Test/autoRevealDependencies/power.dfy → .../LitTest/autoRevealDependencies/power.dfy b/Test/autoRevealDependencies/power.dfy → .../LitTest/autoRevealDependencies/power.dfy
diff --git a/Test/autoRevealDependencies/power.dfy.expect → ...t/autoRevealDependencies/power.dfy.expect b/Test/autoRevealDependencies/power.dfy.expect → ...t/autoRevealDependencies/power.dfy.expect
diff --git a/Test/autoRevealDependencies/subset-types.dfy → ...t/autoRevealDependencies/subset-types.dfy b/Test/autoRevealDependencies/subset-types.dfy → ...t/autoRevealDependencies/subset-types.dfy
diff --git a/...evealDependencies/subset-types.dfy.expect → ...evealDependencies/subset-types.dfy.expect b/...evealDependencies/subset-types.dfy.expect → ...evealDependencies/subset-types.dfy.expect
diff --git a/...utoRevealDependencies/tree-map-simple.dfy → ...utoRevealDependencies/tree-map-simple.dfy b/...utoRevealDependencies/tree-map-simple.dfy → ...utoRevealDependencies/tree-map-simple.dfy
diff --git a/...alDependencies/tree-map-simple.dfy.expect → ...alDependencies/tree-map-simple.dfy.expect b/...alDependencies/tree-map-simple.dfy.expect → ...alDependencies/tree-map-simple.dfy.expect
diff --git a/Test/autoRevealDependencies/typecasting.dfy → ...st/autoRevealDependencies/typecasting.dfy b/Test/autoRevealDependencies/typecasting.dfy → ...st/autoRevealDependencies/typecasting.dfy
diff --git a/...RevealDependencies/typecasting.dfy.expect → ...RevealDependencies/typecasting.dfy.expect b/...RevealDependencies/typecasting.dfy.expect → ...RevealDependencies/typecasting.dfy.expect
diff --git a/...benchmarks/sequence-race/SequenceRace.dfy → ...benchmarks/sequence-race/SequenceRace.dfy b/...benchmarks/sequence-race/SequenceRace.dfy → ...benchmarks/sequence-race/SequenceRace.dfy
diff --git a/...rks/sequence-race/SequenceRace.dfy.expect → ...rks/sequence-race/SequenceRace.dfy.expect b/...rks/sequence-race/SequenceRace.dfy.expect → ...rks/sequence-race/SequenceRace.dfy.expect
diff --git a/...marks/sequence-race/java/build.gradle.kts → ...marks/sequence-race/java/build.gradle.kts b/...marks/sequence-race/java/build.gradle.kts → ...marks/sequence-race/java/build.gradle.kts
diff --git a/...ce/java/gradle/wrapper/gradle-wrapper.jar → ...ce/java/gradle/wrapper/gradle-wrapper.jar b/...ce/java/gradle/wrapper/gradle-wrapper.jar → ...ce/java/gradle/wrapper/gradle-wrapper.jar
diff --git a/.../gradle/wrapper/gradle-wrapper.properties → .../gradle/wrapper/gradle-wrapper.properties b/.../gradle/wrapper/gradle-wrapper.properties → .../gradle/wrapper/gradle-wrapper.properties
diff --git a/Test/benchmarks/sequence-race/java/gradlew → ...est/benchmarks/sequence-race/java/gradlew b/Test/benchmarks/sequence-race/java/gradlew → ...est/benchmarks/sequence-race/java/gradlew
diff --git a/...benchmarks/sequence-race/java/gradlew.bat → ...benchmarks/sequence-race/java/gradlew.bat b/...benchmarks/sequence-race/java/gradlew.bat → ...benchmarks/sequence-race/java/gradlew.bat
diff --git a/...ks/sequence-race/java/settings.gradle.kts → ...ks/sequence-race/java/settings.gradle.kts b/...ks/sequence-race/java/settings.gradle.kts → ...ks/sequence-race/java/settings.gradle.kts
diff --git a/...blogposts/Inputs/TestGenerationShared.dfy → ...blogposts/Inputs/TestGenerationShared.dfy b/...blogposts/Inputs/TestGenerationShared.dfy → ...blogposts/Inputs/TestGenerationShared.dfy
diff --git a/...ationNoInliningEnumerativeDefinitions.dfy → ...ationNoInliningEnumerativeDefinitions.dfy b/...ationNoInliningEnumerativeDefinitions.dfy → ...ationNoInliningEnumerativeDefinitions.dfy
diff --git a/...tionWithInliningQuantifiedDefinitions.dfy → ...tionWithInliningQuantifiedDefinitions.dfy b/...tionWithInliningQuantifiedDefinitions.dfy → ...tionWithInliningQuantifiedDefinitions.dfy
diff --git a/Test/c++/ExternDefs.h → ...stFiles/LitTests/LitTest/c++/ExternDefs.h b/Test/c++/ExternDefs.h → ...stFiles/LitTests/LitTest/c++/ExternDefs.h
diff --git a/Test/c++/Makefile → ...s/TestFiles/LitTests/LitTest/c++/Makefile b/Test/c++/Makefile → ...s/TestFiles/LitTests/LitTest/c++/Makefile
diff --git a/Test/c++/arrays.dfy → ...TestFiles/LitTests/LitTest/c++/arrays.dfy b/Test/c++/arrays.dfy → ...TestFiles/LitTests/LitTest/c++/arrays.dfy
diff --git a/Test/c++/arrays.dfy.expect → ...es/LitTests/LitTest/c++/arrays.dfy.expect b/Test/c++/arrays.dfy.expect → ...es/LitTests/LitTest/c++/arrays.dfy.expect
diff --git a/Test/c++/bit-vectors.dfy → ...iles/LitTests/LitTest/c++/bit-vectors.dfy b/Test/c++/bit-vectors.dfy → ...iles/LitTests/LitTest/c++/bit-vectors.dfy
diff --git a/Test/c++/bit-vectors.dfy.expect → ...tTests/LitTest/c++/bit-vectors.dfy.expect b/Test/c++/bit-vectors.dfy.expect → ...tTests/LitTest/c++/bit-vectors.dfy.expect
diff --git a/Test/c++/class.dfy → .../TestFiles/LitTests/LitTest/c++/class.dfy b/Test/c++/class.dfy → .../TestFiles/LitTests/LitTest/c++/class.dfy
diff --git a/Test/c++/class.dfy.expect → ...les/LitTests/LitTest/c++/class.dfy.expect b/Test/c++/class.dfy.expect → ...les/LitTests/LitTest/c++/class.dfy.expect
diff --git a/Test/c++/class.dfy.java.check → ...LitTests/LitTest/c++/class.dfy.java.check b/Test/c++/class.dfy.java.check → ...LitTests/LitTest/c++/class.dfy.java.check
diff --git a/Test/c++/const.dfy → .../TestFiles/LitTests/LitTest/c++/const.dfy b/Test/c++/const.dfy → .../TestFiles/LitTests/LitTest/c++/const.dfy
diff --git a/Test/c++/const.dfy.expect → ...les/LitTests/LitTest/c++/const.dfy.expect b/Test/c++/const.dfy.expect → ...les/LitTests/LitTest/c++/const.dfy.expect
diff --git a/Test/c++/const.dfy.java.check → ...LitTests/LitTest/c++/const.dfy.java.check b/Test/c++/const.dfy.java.check → ...LitTests/LitTest/c++/const.dfy.java.check
diff --git a/Test/c++/datatypes.dfy → ...tFiles/LitTests/LitTest/c++/datatypes.dfy b/Test/c++/datatypes.dfy → ...tFiles/LitTests/LitTest/c++/datatypes.dfy
diff --git a/Test/c++/datatypes.dfy.expect → ...LitTests/LitTest/c++/datatypes.dfy.expect b/Test/c++/datatypes.dfy.expect → ...LitTests/LitTest/c++/datatypes.dfy.expect
diff --git a/Test/c++/datatypes.dfy.go.check → ...tTests/LitTest/c++/datatypes.dfy.go.check b/Test/c++/datatypes.dfy.go.check → ...tTests/LitTest/c++/datatypes.dfy.go.check
diff --git a/Test/c++/extern.dfy → ...TestFiles/LitTests/LitTest/c++/extern.dfy b/Test/c++/extern.dfy → ...TestFiles/LitTests/LitTest/c++/extern.dfy
diff --git a/Test/c++/extern.dfy.expect → ...es/LitTests/LitTest/c++/extern.dfy.expect b/Test/c++/extern.dfy.expect → ...es/LitTests/LitTest/c++/extern.dfy.expect
diff --git a/Test/c++/functions.dfy → ...tFiles/LitTests/LitTest/c++/functions.dfy b/Test/c++/functions.dfy → ...tFiles/LitTests/LitTest/c++/functions.dfy
diff --git a/Test/c++/functions.dfy.expect → ...LitTests/LitTest/c++/functions.dfy.expect b/Test/c++/functions.dfy.expect → ...LitTests/LitTest/c++/functions.dfy.expect
diff --git a/Test/c++/generic.dfy → ...estFiles/LitTests/LitTest/c++/generic.dfy b/Test/c++/generic.dfy → ...estFiles/LitTests/LitTest/c++/generic.dfy
diff --git a/Test/c++/generic.dfy.expect → ...s/LitTests/LitTest/c++/generic.dfy.expect b/Test/c++/generic.dfy.expect → ...s/LitTests/LitTest/c++/generic.dfy.expect
diff --git a/Test/c++/hello.dfy → .../TestFiles/LitTests/LitTest/c++/hello.dfy b/Test/c++/hello.dfy → .../TestFiles/LitTests/LitTest/c++/hello.dfy
diff --git a/Test/c++/hello.dfy.expect → ...les/LitTests/LitTest/c++/hello.dfy.expect b/Test/c++/hello.dfy.expect → ...les/LitTests/LitTest/c++/hello.dfy.expect
diff --git a/Test/c++/ints.dfy → ...s/TestFiles/LitTests/LitTest/c++/ints.dfy b/Test/c++/ints.dfy → ...s/TestFiles/LitTests/LitTest/c++/ints.dfy
diff --git a/Test/c++/ints.dfy.expect → ...iles/LitTests/LitTest/c++/ints.dfy.expect b/Test/c++/ints.dfy.expect → ...iles/LitTests/LitTest/c++/ints.dfy.expect
diff --git a/Test/c++/maps.dfy → ...s/TestFiles/LitTests/LitTest/c++/maps.dfy b/Test/c++/maps.dfy → ...s/TestFiles/LitTests/LitTest/c++/maps.dfy
diff --git a/Test/c++/maps.dfy.cpp.expect → .../LitTests/LitTest/c++/maps.dfy.cpp.expect b/Test/c++/maps.dfy.cpp.expect → .../LitTests/LitTest/c++/maps.dfy.cpp.expect
diff --git a/Test/c++/maps.dfy.expect → ...iles/LitTests/LitTest/c++/maps.dfy.expect b/Test/c++/maps.dfy.expect → ...iles/LitTests/LitTest/c++/maps.dfy.expect
diff --git a/Test/c++/recursion.dfy → ...tFiles/LitTests/LitTest/c++/recursion.dfy b/Test/c++/recursion.dfy → ...tFiles/LitTests/LitTest/c++/recursion.dfy
diff --git a/Test/c++/recursion.dfy.expect → ...LitTests/LitTest/c++/recursion.dfy.expect b/Test/c++/recursion.dfy.expect → ...LitTests/LitTest/c++/recursion.dfy.expect
diff --git a/Test/c++/returns.dfy → ...estFiles/LitTests/LitTest/c++/returns.dfy b/Test/c++/returns.dfy → ...estFiles/LitTests/LitTest/c++/returns.dfy
diff --git a/Test/c++/returns.dfy.expect → ...s/LitTests/LitTest/c++/returns.dfy.expect b/Test/c++/returns.dfy.expect → ...s/LitTests/LitTest/c++/returns.dfy.expect
diff --git a/Test/c++/run_cpp_tests.py → ...les/LitTests/LitTest/c++/run_cpp_tests.py b/Test/c++/run_cpp_tests.py → ...les/LitTests/LitTest/c++/run_cpp_tests.py
diff --git a/Test/c++/seqs.dfy → ...s/TestFiles/LitTests/LitTest/c++/seqs.dfy b/Test/c++/seqs.dfy → ...s/TestFiles/LitTests/LitTest/c++/seqs.dfy
diff --git a/Test/c++/seqs.dfy.expect → ...iles/LitTests/LitTest/c++/seqs.dfy.expect b/Test/c++/seqs.dfy.expect → ...iles/LitTests/LitTest/c++/seqs.dfy.expect
diff --git a/Test/c++/sets.dfy → ...s/TestFiles/LitTests/LitTest/c++/sets.dfy b/Test/c++/sets.dfy → ...s/TestFiles/LitTests/LitTest/c++/sets.dfy
diff --git a/Test/c++/sets.dfy.expect → ...iles/LitTests/LitTest/c++/sets.dfy.expect b/Test/c++/sets.dfy.expect → ...iles/LitTests/LitTest/c++/sets.dfy.expect
diff --git a/Test/c++/tuple.dfy → .../TestFiles/LitTests/LitTest/c++/tuple.dfy b/Test/c++/tuple.dfy → .../TestFiles/LitTests/LitTest/c++/tuple.dfy
diff --git a/Test/c++/tuple.dfy.expect → ...les/LitTests/LitTest/c++/tuple.dfy.expect b/Test/c++/tuple.dfy.expect → ...les/LitTests/LitTest/c++/tuple.dfy.expect
diff --git a/Test/c++/while.dfy → .../TestFiles/LitTests/LitTest/c++/while.dfy b/Test/c++/while.dfy → .../TestFiles/LitTests/LitTest/c++/while.dfy
diff --git a/Test/c++/while.dfy.expect → ...les/LitTests/LitTest/c++/while.dfy.expect b/Test/c++/while.dfy.expect → ...les/LitTests/LitTest/c++/while.dfy.expect
diff --git a/Test/c++/while.dfy.java.check → ...LitTests/LitTest/c++/while.dfy.java.check b/Test/c++/while.dfy.java.check → ...LitTests/LitTest/c++/while.dfy.java.check
diff --git a/Test/clean.py → ...Tests/TestFiles/LitTests/LitTest/clean.py b/Test/clean.py → ...Tests/TestFiles/LitTests/LitTest/clean.py
diff --git a/Test/cli/badArguments.dfy → ...les/LitTests/LitTest/cli/badArguments.dfy b/Test/cli/badArguments.dfy → ...les/LitTests/LitTest/cli/badArguments.dfy
diff --git a/Test/cli/badArguments.dfy.expect → ...Tests/LitTest/cli/badArguments.dfy.expect b/Test/cli/badArguments.dfy.expect → ...Tests/LitTest/cli/badArguments.dfy.expect
diff --git a/Test/cli/badProverPath.dfy → ...es/LitTests/LitTest/cli/badProverPath.dfy b/Test/cli/badProverPath.dfy → ...es/LitTests/LitTest/cli/badProverPath.dfy
diff --git a/Test/cli/customMain.dfy → ...Files/LitTests/LitTest/cli/customMain.dfy b/Test/cli/customMain.dfy → ...Files/LitTests/LitTest/cli/customMain.dfy
diff --git a/Test/cli/customMain.dfy.expect → ...itTests/LitTest/cli/customMain.dfy.expect b/Test/cli/customMain.dfy.expect → ...itTests/LitTest/cli/customMain.dfy.expect
diff --git a/Test/cli/diagnosticsFormats.dfy → ...tTests/LitTest/cli/diagnosticsFormats.dfy b/Test/cli/diagnosticsFormats.dfy → ...tTests/LitTest/cli/diagnosticsFormats.dfy
diff --git a/Test/cli/diagnosticsFormats.dfy.expect → ...LitTest/cli/diagnosticsFormats.dfy.expect b/Test/cli/diagnosticsFormats.dfy.expect → ...LitTest/cli/diagnosticsFormats.dfy.expect
diff --git a/Test/cli/errorLimit.dfy → ...Files/LitTests/LitTest/cli/errorLimit.dfy b/Test/cli/errorLimit.dfy → ...Files/LitTests/LitTest/cli/errorLimit.dfy
diff --git a/Test/cli/errorLimit.dfy.expect → ...itTests/LitTest/cli/errorLimit.dfy.expect b/Test/cli/errorLimit.dfy.expect → ...itTests/LitTest/cli/errorLimit.dfy.expect
diff --git a/Test/cli/help.dfy → ...s/TestFiles/LitTests/LitTest/cli/help.dfy b/Test/cli/help.dfy → ...s/TestFiles/LitTests/LitTest/cli/help.dfy
diff --git a/...i/libraryOption/Inputs/brokenProducer.dfy → ...i/libraryOption/Inputs/brokenProducer.dfy b/...i/libraryOption/Inputs/brokenProducer.dfy → ...i/libraryOption/Inputs/brokenProducer.dfy
diff --git a/Test/cli/libraryOption/libraryOption.dfy → ...tTest/cli/libraryOption/libraryOption.dfy b/Test/cli/libraryOption/libraryOption.dfy → ...tTest/cli/libraryOption/libraryOption.dfy
diff --git a/...li/libraryOption/libraryOption.dfy.expect → ...li/libraryOption/libraryOption.dfy.expect b/...li/libraryOption/libraryOption.dfy.expect → ...li/libraryOption/libraryOption.dfy.expect
diff --git a/Test/cli/multipleBoogieArguments.dfy → ...s/LitTest/cli/multipleBoogieArguments.dfy b/Test/cli/multipleBoogieArguments.dfy → ...s/LitTest/cli/multipleBoogieArguments.dfy
diff --git a/Test/cli/multipleBoogieArguments.dfy.expect → ...st/cli/multipleBoogieArguments.dfy.expect b/Test/cli/multipleBoogieArguments.dfy.expect → ...st/cli/multipleBoogieArguments.dfy.expect
diff --git a/Test/cli/projectFile/badTypes/badTypes.dfy → ...est/cli/projectFile/badTypes/badTypes.dfy b/Test/cli/projectFile/badTypes/badTypes.dfy → ...est/cli/projectFile/badTypes/badTypes.dfy
diff --git a/Test/cli/projectFile/badTypes/dfyconfig.toml → ...t/cli/projectFile/badTypes/dfyconfig.toml b/Test/cli/projectFile/badTypes/dfyconfig.toml → ...t/cli/projectFile/badTypes/dfyconfig.toml
diff --git a/Test/cli/projectFile/broken/dfyconfig.toml → ...est/cli/projectFile/broken/dfyconfig.toml b/Test/cli/projectFile/broken/dfyconfig.toml → ...est/cli/projectFile/broken/dfyconfig.toml
diff --git a/...cli/projectFile/broken/invalidOption.toml → ...cli/projectFile/broken/invalidOption.toml b/...cli/projectFile/broken/invalidOption.toml → ...cli/projectFile/broken/invalidOption.toml
diff --git a/Test/cli/projectFile/dfyconfig.toml → ...ts/LitTest/cli/projectFile/dfyconfig.toml b/Test/cli/projectFile/dfyconfig.toml → ...ts/LitTest/cli/projectFile/dfyconfig.toml
diff --git a/.../cli/projectFile/libraries/dfyconfig.toml → .../cli/projectFile/libraries/dfyconfig.toml b/.../cli/projectFile/libraries/dfyconfig.toml → .../cli/projectFile/libraries/dfyconfig.toml
diff --git a/...cli/projectFile/libraries/usesLibrary.dfy → ...cli/projectFile/libraries/usesLibrary.dfy b/...cli/projectFile/libraries/usesLibrary.dfy → ...cli/projectFile/libraries/usesLibrary.dfy
diff --git a/...jectFile/libraries/usesLibrary.dfy.expect → ...jectFile/libraries/usesLibrary.dfy.expect b/...jectFile/libraries/usesLibrary.dfy.expect → ...jectFile/libraries/usesLibrary.dfy.expect
diff --git a/...cli/projectFile/libraries/wrappersLib.dfy → ...cli/projectFile/libraries/wrappersLib.dfy b/...cli/projectFile/libraries/wrappersLib.dfy → ...cli/projectFile/libraries/wrappersLib.dfy
diff --git a/...cli/projectFile/noIncludes/dfyconfig.toml → ...cli/projectFile/noIncludes/dfyconfig.toml b/...cli/projectFile/noIncludes/dfyconfig.toml → ...cli/projectFile/noIncludes/dfyconfig.toml
diff --git a/.../cli/projectFile/noIncludes/src/input.dfy → .../cli/projectFile/noIncludes/src/input.dfy b/.../cli/projectFile/noIncludes/src/input.dfy → .../cli/projectFile/noIncludes/src/input.dfy
diff --git a/...e/noIncludes/src/moreNested/moreInput.dfy → ...e/noIncludes/src/moreNested/moreInput.dfy b/...e/noIncludes/src/moreNested/moreInput.dfy → ...e/noIncludes/src/moreNested/moreInput.dfy
diff --git a/.../cli/projectFile/noOptions/dfyconfig.toml → .../cli/projectFile/noOptions/dfyconfig.toml b/.../cli/projectFile/noOptions/dfyconfig.toml → .../cli/projectFile/noOptions/dfyconfig.toml
diff --git a/Test/cli/projectFile/noOptions/input.dfy → ...tTest/cli/projectFile/noOptions/input.dfy b/Test/cli/projectFile/noOptions/input.dfy → ...tTest/cli/projectFile/noOptions/input.dfy
diff --git a/...li/projectFile/noOptions/input.dfy.expect → ...li/projectFile/noOptions/input.dfy.expect b/...li/projectFile/noOptions/input.dfy.expect → ...li/projectFile/noOptions/input.dfy.expect
diff --git a/Test/cli/projectFile/notInput.dfy → ...ests/LitTest/cli/projectFile/notInput.dfy b/Test/cli/projectFile/notInput.dfy → ...ests/LitTest/cli/projectFile/notInput.dfy
diff --git a/Test/cli/projectFile/projectFile.dfy → ...s/LitTest/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy → ...s/LitTest/cli/projectFile/projectFile.dfy
diff --git a/Test/cli/projectFile/projectFile.dfy.expect → ...st/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect → ...st/cli/projectFile/projectFile.dfy.expect
diff --git a/Test/cli/projectFile/projectFileRun.dfy → ...itTest/cli/projectFile/projectFileRun.dfy b/Test/cli/projectFile/projectFileRun.dfy → ...itTest/cli/projectFile/projectFileRun.dfy
diff --git a/...cli/projectFile/projectFileRun.dfy.expect → ...cli/projectFile/projectFileRun.dfy.expect b/...cli/projectFile/projectFileRun.dfy.expect → ...cli/projectFile/projectFileRun.dfy.expect
diff --git a/Test/cli/projectFile/src/excluded.dfy → .../LitTest/cli/projectFile/src/excluded.dfy b/Test/cli/projectFile/src/excluded.dfy → .../LitTest/cli/projectFile/src/excluded.dfy
diff --git a/Test/cli/projectFile/src/input.dfy → ...sts/LitTest/cli/projectFile/src/input.dfy b/Test/cli/projectFile/src/input.dfy → ...sts/LitTest/cli/projectFile/src/input.dfy
diff --git a/Test/cli/proverPath.dfy → ...Files/LitTests/LitTest/cli/proverPath.dfy b/Test/cli/proverPath.dfy → ...Files/LitTests/LitTest/cli/proverPath.dfy
diff --git a/Test/cli/proverPath.dfy.expect → ...itTests/LitTest/cli/proverPath.dfy.expect b/Test/cli/proverPath.dfy.expect → ...itTests/LitTest/cli/proverPath.dfy.expect
diff --git a/Test/cli/resolve.dfy → ...estFiles/LitTests/LitTest/cli/resolve.dfy b/Test/cli/resolve.dfy → ...estFiles/LitTests/LitTest/cli/resolve.dfy
diff --git a/Test/cli/resolve.dfy.expect → ...s/LitTests/LitTest/cli/resolve.dfy.expect b/Test/cli/resolve.dfy.expect → ...s/LitTests/LitTest/cli/resolve.dfy.expect
diff --git a/Test/cli/solverLog.dfy → ...tFiles/LitTests/LitTest/cli/solverLog.dfy b/Test/cli/solverLog.dfy → ...tFiles/LitTests/LitTest/cli/solverLog.dfy
diff --git a/Test/cli/solverLog.dfy.expect → ...LitTests/LitTest/cli/solverLog.dfy.expect b/Test/cli/solverLog.dfy.expect → ...LitTests/LitTest/cli/solverLog.dfy.expect
diff --git a/Test/cli/solverOpt.dfy → ...tFiles/LitTests/LitTest/cli/solverOpt.dfy b/Test/cli/solverOpt.dfy → ...tFiles/LitTests/LitTest/cli/solverOpt.dfy
diff --git a/Test/cli/zeroCores.dfy → ...tFiles/LitTests/LitTest/cli/zeroCores.dfy b/Test/cli/zeroCores.dfy → ...tFiles/LitTests/LitTest/cli/zeroCores.dfy
diff --git a/Test/cli/zeroCores.dfy.expect → ...LitTests/LitTest/cli/zeroCores.dfy.expect b/Test/cli/zeroCores.dfy.expect → ...LitTests/LitTest/cli/zeroCores.dfy.expect
diff --git a/Test/cloudmake/CloudMake-CachedBuilds.dfy → ...Test/cloudmake/CloudMake-CachedBuilds.dfy b/Test/cloudmake/CloudMake-CachedBuilds.dfy → ...Test/cloudmake/CloudMake-CachedBuilds.dfy
diff --git a/...oudmake/CloudMake-CachedBuilds.dfy.expect → ...oudmake/CloudMake-CachedBuilds.dfy.expect b/...oudmake/CloudMake-CachedBuilds.dfy.expect → ...oudmake/CloudMake-CachedBuilds.dfy.expect
diff --git a/.../cloudmake/CloudMake-ConsistentBuilds.dfy → .../cloudmake/CloudMake-ConsistentBuilds.dfy b/.../cloudmake/CloudMake-ConsistentBuilds.dfy → .../cloudmake/CloudMake-ConsistentBuilds.dfy
diff --git a/...ake/CloudMake-ConsistentBuilds.dfy.expect → ...ake/CloudMake-ConsistentBuilds.dfy.expect b/...ake/CloudMake-ConsistentBuilds.dfy.expect → ...ake/CloudMake-ConsistentBuilds.dfy.expect
diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy → ...st/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy → ...st/cloudmake/CloudMake-ParallelBuilds.dfy
diff --git a/...dmake/CloudMake-ParallelBuilds.dfy.expect → ...dmake/CloudMake-ParallelBuilds.dfy.expect b/...dmake/CloudMake-ParallelBuilds.dfy.expect → ...dmake/CloudMake-ParallelBuilds.dfy.expect
diff --git a/Test/comp/.gitignore → ...estFiles/LitTests/LitTest/comp/.gitignore b/Test/comp/.gitignore → ...estFiles/LitTests/LitTest/comp/.gitignore
diff --git a/Test/comp/AllDafny.java → ...Files/LitTests/LitTest/comp/AllDafny.java b/Test/comp/AllDafny.java → ...Files/LitTests/LitTest/comp/AllDafny.java
diff --git a/Test/comp/AllExtern.java → ...iles/LitTests/LitTest/comp/AllExtern.java b/Test/comp/AllExtern.java → ...iles/LitTests/LitTest/comp/AllExtern.java
diff --git a/Test/comp/Arrays.dfy → ...estFiles/LitTests/LitTest/comp/Arrays.dfy b/Test/comp/Arrays.dfy → ...estFiles/LitTests/LitTest/comp/Arrays.dfy
diff --git a/Test/comp/Arrays.dfy.expect → ...s/LitTests/LitTest/comp/Arrays.dfy.expect b/Test/comp/Arrays.dfy.expect → ...s/LitTests/LitTest/comp/Arrays.dfy.expect
diff --git a/Test/comp/Arrays.dfy.go.expect → ...itTests/LitTest/comp/Arrays.dfy.go.expect b/Test/comp/Arrays.dfy.go.expect → ...itTests/LitTest/comp/Arrays.dfy.go.expect
diff --git a/Test/comp/AsIs-Compile.dfy → ...es/LitTests/LitTest/comp/AsIs-Compile.dfy b/Test/comp/AsIs-Compile.dfy → ...es/LitTests/LitTest/comp/AsIs-Compile.dfy
diff --git a/Test/comp/AsIs-Compile.dfy.expect → ...ests/LitTest/comp/AsIs-Compile.dfy.expect b/Test/comp/AsIs-Compile.dfy.expect → ...ests/LitTest/comp/AsIs-Compile.dfy.expect
diff --git a/Test/comp/AutoInit.dfy → ...tFiles/LitTests/LitTest/comp/AutoInit.dfy b/Test/comp/AutoInit.dfy → ...tFiles/LitTests/LitTest/comp/AutoInit.dfy
diff --git a/Test/comp/AutoInit.dfy.expect → ...LitTests/LitTest/comp/AutoInit.dfy.expect b/Test/comp/AutoInit.dfy.expect → ...LitTests/LitTest/comp/AutoInit.dfy.expect
diff --git a/Test/comp/BranchCoverage.dfy → .../LitTests/LitTest/comp/BranchCoverage.dfy b/Test/comp/BranchCoverage.dfy → .../LitTests/LitTest/comp/BranchCoverage.dfy
diff --git a/Test/comp/BranchCoverage.dfy.expect → ...ts/LitTest/comp/BranchCoverage.dfy.expect b/Test/comp/BranchCoverage.dfy.expect → ...ts/LitTest/comp/BranchCoverage.dfy.expect
diff --git a/Test/comp/BranchCoverage.py → ...s/LitTests/LitTest/comp/BranchCoverage.py b/Test/comp/BranchCoverage.py → ...s/LitTests/LitTest/comp/BranchCoverage.py
diff --git a/Test/comp/BranchCoverage2.cs → .../LitTests/LitTest/comp/BranchCoverage2.cs b/Test/comp/BranchCoverage2.cs → .../LitTests/LitTest/comp/BranchCoverage2.cs
diff --git a/Test/comp/BranchCoverage3.js → .../LitTests/LitTest/comp/BranchCoverage3.js b/Test/comp/BranchCoverage3.js → .../LitTests/LitTest/comp/BranchCoverage3.js
diff --git a/Test/comp/BranchCoverage4.go → .../LitTests/LitTest/comp/BranchCoverage4.go b/Test/comp/BranchCoverage4.go → .../LitTests/LitTest/comp/BranchCoverage4.go
diff --git a/Test/comp/ByMethodCompilation.dfy → ...ests/LitTest/comp/ByMethodCompilation.dfy b/Test/comp/ByMethodCompilation.dfy → ...ests/LitTest/comp/ByMethodCompilation.dfy
diff --git a/Test/comp/ByMethodCompilation.dfy.expect → ...tTest/comp/ByMethodCompilation.dfy.expect b/Test/comp/ByMethodCompilation.dfy.expect → ...tTest/comp/ByMethodCompilation.dfy.expect
diff --git a/Test/comp/CSharpStyling.dfy → ...s/LitTests/LitTest/comp/CSharpStyling.dfy b/Test/comp/CSharpStyling.dfy → ...s/LitTests/LitTest/comp/CSharpStyling.dfy
diff --git a/Test/comp/CSharpStyling.dfy.expect → ...sts/LitTest/comp/CSharpStyling.dfy.expect b/Test/comp/CSharpStyling.dfy.expect → ...sts/LitTest/comp/CSharpStyling.dfy.expect
diff --git a/Test/comp/CSharpStyling2.cs → ...s/LitTests/LitTest/comp/CSharpStyling2.cs b/Test/comp/CSharpStyling2.cs → ...s/LitTests/LitTest/comp/CSharpStyling2.cs
diff --git a/Test/comp/Calls.dfy → ...TestFiles/LitTests/LitTest/comp/Calls.dfy b/Test/comp/Calls.dfy → ...TestFiles/LitTests/LitTest/comp/Calls.dfy
diff --git a/Test/comp/Calls.dfy.expect → ...es/LitTests/LitTest/comp/Calls.dfy.expect b/Test/comp/Calls.dfy.expect → ...es/LitTests/LitTest/comp/Calls.dfy.expect
diff --git a/Test/comp/Class.dfy → ...TestFiles/LitTests/LitTest/comp/Class.dfy b/Test/comp/Class.dfy → ...TestFiles/LitTests/LitTest/comp/Class.dfy
diff --git a/Test/comp/Class.dfy.expect → ...es/LitTests/LitTest/comp/Class.dfy.expect b/Test/comp/Class.dfy.expect → ...es/LitTests/LitTest/comp/Class.dfy.expect
diff --git a/Test/comp/CodeCoverage.java → ...s/LitTests/LitTest/comp/CodeCoverage.java b/Test/comp/CodeCoverage.java → ...s/LitTests/LitTest/comp/CodeCoverage.java
diff --git a/Test/comp/Collections.dfy → ...les/LitTests/LitTest/comp/Collections.dfy b/Test/comp/Collections.dfy → ...les/LitTests/LitTest/comp/Collections.dfy
diff --git a/Test/comp/Collections.dfy.expect → ...Tests/LitTest/comp/Collections.dfy.expect b/Test/comp/Collections.dfy.expect → ...Tests/LitTest/comp/Collections.dfy.expect
diff --git a/Test/comp/Collections.dfy.go.expect → ...ts/LitTest/comp/Collections.dfy.go.expect b/Test/comp/Collections.dfy.go.expect → ...ts/LitTest/comp/Collections.dfy.go.expect
diff --git a/Test/comp/Collections.dfy.java.expect → .../LitTest/comp/Collections.dfy.java.expect b/Test/comp/Collections.dfy.java.expect → .../LitTest/comp/Collections.dfy.java.expect
diff --git a/Test/comp/Collections.dfy.js.expect → ...ts/LitTest/comp/Collections.dfy.js.expect b/Test/comp/Collections.dfy.js.expect → ...ts/LitTest/comp/Collections.dfy.js.expect
diff --git a/Test/comp/Collections.dfy.py.expect → ...ts/LitTest/comp/Collections.dfy.py.expect b/Test/comp/Collections.dfy.py.expect → ...ts/LitTest/comp/Collections.dfy.py.expect
diff --git a/Test/comp/CompileWithArguments.dfy → ...sts/LitTest/comp/CompileWithArguments.dfy b/Test/comp/CompileWithArguments.dfy → ...sts/LitTest/comp/CompileWithArguments.dfy
diff --git a/Test/comp/CompileWithArguments.dfy.expect → ...Test/comp/CompileWithArguments.dfy.expect b/Test/comp/CompileWithArguments.dfy.expect → ...Test/comp/CompileWithArguments.dfy.expect
diff --git a/Test/comp/CompileWithArgumentsFail.dfy → ...LitTest/comp/CompileWithArgumentsFail.dfy b/Test/comp/CompileWithArgumentsFail.dfy → ...LitTest/comp/CompileWithArgumentsFail.dfy
diff --git a/.../comp/CompileWithArgumentsFail.dfy.expect → .../comp/CompileWithArgumentsFail.dfy.expect b/.../comp/CompileWithArgumentsFail.dfy.expect → .../comp/CompileWithArgumentsFail.dfy.expect
diff --git a/Test/comp/CompileWithArgumentsFail2.dfy → ...itTest/comp/CompileWithArgumentsFail2.dfy b/Test/comp/CompileWithArgumentsFail2.dfy → ...itTest/comp/CompileWithArgumentsFail2.dfy
diff --git a/...comp/CompileWithArgumentsFail2.dfy.expect → ...comp/CompileWithArgumentsFail2.dfy.expect b/...comp/CompileWithArgumentsFail2.dfy.expect → ...comp/CompileWithArgumentsFail2.dfy.expect
diff --git a/Test/comp/Comprehensions.dfy → .../LitTests/LitTest/comp/Comprehensions.dfy b/Test/comp/Comprehensions.dfy → .../LitTests/LitTest/comp/Comprehensions.dfy
diff --git a/Test/comp/Comprehensions.dfy.expect → ...ts/LitTest/comp/Comprehensions.dfy.expect b/Test/comp/Comprehensions.dfy.expect → ...ts/LitTest/comp/Comprehensions.dfy.expect
diff --git a/Test/comp/Comprehensions.dfy.py.expect → ...LitTest/comp/Comprehensions.dfy.py.expect b/Test/comp/Comprehensions.dfy.py.expect → ...LitTest/comp/Comprehensions.dfy.py.expect
diff --git a/Test/comp/ComprehensionsNewSyntax.dfy → .../LitTest/comp/ComprehensionsNewSyntax.dfy b/Test/comp/ComprehensionsNewSyntax.dfy → .../LitTest/comp/ComprehensionsNewSyntax.dfy
diff --git a/Test/comp/ComprehensionsNewSyntax.dfy.expect → ...t/comp/ComprehensionsNewSyntax.dfy.expect b/Test/comp/ComprehensionsNewSyntax.dfy.expect → ...t/comp/ComprehensionsNewSyntax.dfy.expect
diff --git a/...omp/ComprehensionsNewSyntax.dfy.py.expect → ...omp/ComprehensionsNewSyntax.dfy.py.expect b/...omp/ComprehensionsNewSyntax.dfy.py.expect → ...omp/ComprehensionsNewSyntax.dfy.py.expect
diff --git a/Test/comp/Conversions.java → ...es/LitTests/LitTest/comp/Conversions.java b/Test/comp/Conversions.java → ...es/LitTests/LitTest/comp/Conversions.java
diff --git a/Test/comp/CovariantCollections.dfy → ...sts/LitTest/comp/CovariantCollections.dfy b/Test/comp/CovariantCollections.dfy → ...sts/LitTest/comp/CovariantCollections.dfy
diff --git a/Test/comp/CovariantCollections.dfy.expect → ...Test/comp/CovariantCollections.dfy.expect b/Test/comp/CovariantCollections.dfy.expect → ...Test/comp/CovariantCollections.dfy.expect
diff --git a/Test/comp/Datatype.dfy → ...tFiles/LitTests/LitTest/comp/Datatype.dfy b/Test/comp/Datatype.dfy → ...tFiles/LitTests/LitTest/comp/Datatype.dfy
diff --git a/Test/comp/Datatype.dfy.expect → ...LitTests/LitTest/comp/Datatype.dfy.expect b/Test/comp/Datatype.dfy.expect → ...LitTests/LitTest/comp/Datatype.dfy.expect
diff --git a/Test/comp/Datatype.dfy.java.expect → ...sts/LitTest/comp/Datatype.dfy.java.expect b/Test/comp/Datatype.dfy.java.expect → ...sts/LitTest/comp/Datatype.dfy.java.expect
diff --git a/Test/comp/Datatype.dfy.py.expect → ...Tests/LitTest/comp/Datatype.dfy.py.expect b/Test/comp/Datatype.dfy.py.expect → ...Tests/LitTest/comp/Datatype.dfy.py.expect
diff --git a/Test/comp/DefaultParameters-Compile.dfy → ...itTest/comp/DefaultParameters-Compile.dfy b/Test/comp/DefaultParameters-Compile.dfy → ...itTest/comp/DefaultParameters-Compile.dfy
diff --git a/...comp/DefaultParameters-Compile.dfy.expect → ...comp/DefaultParameters-Compile.dfy.expect b/...comp/DefaultParameters-Compile.dfy.expect → ...comp/DefaultParameters-Compile.dfy.expect
diff --git a/Test/comp/DowncastClone.dfy → ...s/LitTests/LitTest/comp/DowncastClone.dfy b/Test/comp/DowncastClone.dfy → ...s/LitTests/LitTest/comp/DowncastClone.dfy
diff --git a/Test/comp/DowncastClone.dfy.expect → ...sts/LitTest/comp/DowncastClone.dfy.expect b/Test/comp/DowncastClone.dfy.expect → ...sts/LitTest/comp/DowncastClone.dfy.expect
diff --git a/Test/comp/ErasableTypeWrappers.dfy → ...sts/LitTest/comp/ErasableTypeWrappers.dfy b/Test/comp/ErasableTypeWrappers.dfy → ...sts/LitTest/comp/ErasableTypeWrappers.dfy
diff --git a/Test/comp/ErasableTypeWrappers.dfy.expect → ...Test/comp/ErasableTypeWrappers.dfy.expect b/Test/comp/ErasableTypeWrappers.dfy.expect → ...Test/comp/ErasableTypeWrappers.dfy.expect
diff --git a/Test/comp/EuclideanDivision.dfy → ...tTests/LitTest/comp/EuclideanDivision.dfy b/Test/comp/EuclideanDivision.dfy → ...tTests/LitTest/comp/EuclideanDivision.dfy
diff --git a/Test/comp/EuclideanDivision.dfy.expect → ...LitTest/comp/EuclideanDivision.dfy.expect b/Test/comp/EuclideanDivision.dfy.expect → ...LitTest/comp/EuclideanDivision.dfy.expect
diff --git a/Test/comp/Extern.dfy → ...estFiles/LitTests/LitTest/comp/Extern.dfy b/Test/comp/Extern.dfy → ...estFiles/LitTests/LitTest/comp/Extern.dfy
diff --git a/Test/comp/Extern.dfy.expect → ...s/LitTests/LitTest/comp/Extern.dfy.expect b/Test/comp/Extern.dfy.expect → ...s/LitTests/LitTest/comp/Extern.dfy.expect
diff --git a/Test/comp/Extern2.cs → ...estFiles/LitTests/LitTest/comp/Extern2.cs b/Test/comp/Extern2.cs → ...estFiles/LitTests/LitTest/comp/Extern2.cs
diff --git a/Test/comp/Extern3.js → ...estFiles/LitTests/LitTest/comp/Extern3.js b/Test/comp/Extern3.js → ...estFiles/LitTests/LitTest/comp/Extern3.js
diff --git a/Test/comp/Extern4.go → ...estFiles/LitTests/LitTest/comp/Extern4.go b/Test/comp/Extern4.go → ...estFiles/LitTests/LitTest/comp/Extern4.go
diff --git a/Test/comp/Extern5.py → ...estFiles/LitTests/LitTest/comp/Extern5.py b/Test/comp/Extern5.py → ...estFiles/LitTests/LitTest/comp/Extern5.py
diff --git a/Test/comp/ExternCopyFromTrait.dfy → ...ests/LitTest/comp/ExternCopyFromTrait.dfy b/Test/comp/ExternCopyFromTrait.dfy → ...ests/LitTest/comp/ExternCopyFromTrait.dfy
diff --git a/Test/comp/ExternCopyFromTrait.dfy.expect → ...tTest/comp/ExternCopyFromTrait.dfy.expect b/Test/comp/ExternCopyFromTrait.dfy.expect → ...tTest/comp/ExternCopyFromTrait.dfy.expect
diff --git a/Test/comp/ExternCopyFromTraitLibrary.cs → ...itTest/comp/ExternCopyFromTraitLibrary.cs b/Test/comp/ExternCopyFromTraitLibrary.cs → ...itTest/comp/ExternCopyFromTraitLibrary.cs
diff --git a/Test/comp/ExternCtors-externs/Class.java → ...tTest/comp/ExternCtors-externs/Class.java b/Test/comp/ExternCtors-externs/Class.java → ...tTest/comp/ExternCtors-externs/Class.java
diff --git a/Test/comp/ExternCtors-externs/Library.cs → ...tTest/comp/ExternCtors-externs/Library.cs b/Test/comp/ExternCtors-externs/Library.cs → ...tTest/comp/ExternCtors-externs/Library.cs
diff --git a/Test/comp/ExternCtors-externs/Library.go → ...tTest/comp/ExternCtors-externs/Library.go b/Test/comp/ExternCtors-externs/Library.go → ...tTest/comp/ExternCtors-externs/Library.go
diff --git a/Test/comp/ExternCtors-externs/Library.js → ...tTest/comp/ExternCtors-externs/Library.js b/Test/comp/ExternCtors-externs/Library.js → ...tTest/comp/ExternCtors-externs/Library.js
diff --git a/Test/comp/ExternCtors-externs/Library.py → ...tTest/comp/ExternCtors-externs/Library.py b/Test/comp/ExternCtors-externs/Library.py → ...tTest/comp/ExternCtors-externs/Library.py
diff --git a/Test/comp/ExternCtors.dfy → ...les/LitTests/LitTest/comp/ExternCtors.dfy b/Test/comp/ExternCtors.dfy → ...les/LitTests/LitTest/comp/ExternCtors.dfy
diff --git a/Test/comp/ExternCtors.dfy.expect → ...Tests/LitTest/comp/ExternCtors.dfy.expect b/Test/comp/ExternCtors.dfy.expect → ...Tests/LitTest/comp/ExternCtors.dfy.expect
diff --git a/Test/comp/ExternDLL.dfy → ...Files/LitTests/LitTest/comp/ExternDLL.dfy b/Test/comp/ExternDLL.dfy → ...Files/LitTests/LitTest/comp/ExternDLL.dfy
diff --git a/Test/comp/ExternDLL.dfy.expect → ...itTests/LitTest/comp/ExternDLL.dfy.expect b/Test/comp/ExternDLL.dfy.expect → ...itTests/LitTest/comp/ExternDLL.dfy.expect
diff --git a/Test/comp/ExternDLL2.cs → ...Files/LitTests/LitTest/comp/ExternDLL2.cs b/Test/comp/ExternDLL2.cs → ...Files/LitTests/LitTest/comp/ExternDLL2.cs
diff --git a/Test/comp/ExternDafnyString.dfy → ...tTests/LitTest/comp/ExternDafnyString.dfy b/Test/comp/ExternDafnyString.dfy → ...tTests/LitTest/comp/ExternDafnyString.dfy
diff --git a/Test/comp/ExternDafnyString.dfy.expect → ...LitTest/comp/ExternDafnyString.dfy.expect b/Test/comp/ExternDafnyString.dfy.expect → ...LitTest/comp/ExternDafnyString.dfy.expect
diff --git a/Test/comp/ExternDafnyString.java → ...Tests/LitTest/comp/ExternDafnyString.java b/Test/comp/ExternDafnyString.java → ...Tests/LitTest/comp/ExternDafnyString.java
diff --git a/Test/comp/ExternHelloLibrary.cs → ...tTests/LitTest/comp/ExternHelloLibrary.cs b/Test/comp/ExternHelloLibrary.cs → ...tTests/LitTest/comp/ExternHelloLibrary.cs
diff --git a/Test/comp/ExternHelloLibrary.dll → ...Tests/LitTest/comp/ExternHelloLibrary.dll b/Test/comp/ExternHelloLibrary.dll → ...Tests/LitTest/comp/ExternHelloLibrary.dll