diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 4 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 2 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 4 |
3 files changed, 5 insertions, 5 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index f2148158..6f56f241 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1248,8 +1248,8 @@ namespace Microsoft.Boogie { }
if (TheProverFactory == null) {
- TheProverFactory = ProverFactory.Load("SMTLIB");
- ProverName = "SMTLIB".ToUpper();
+ TheProverFactory = ProverFactory.Load("SMTLib");
+ ProverName = "SMTLib".ToUpper();
}
if (vcVariety == VCVariety.Unspecified) {
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 5b0f7e3e..b375efd9 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -125,7 +125,7 @@ <Compile Include="CrossThreadInvariantProcessor.cs" />
<Compile Include="EnabledToPredicateVisitor.cs" />
<Compile Include="CommandLineOptions.cs" />
- <Compile Include="ElementEncodingraceInstrumenter.cs" />
+ <Compile Include="ElementEncodingRaceInstrumenter.cs" />
<Compile Include="GPUVerifier.cs" />
<Compile Include="INonLocalState.cs" />
<Compile Include="IRaceInstrumenter.cs" />
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 635280d1..0a0e37a2 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -563,7 +563,7 @@ namespace Microsoft.Boogie.SMTLib if (node.Type.BvBits % 8 == 0) {
wr.Write("#x");
for (var pos = node.Type.BvBits / 8 - 1; pos >= 0; pos--) {
- var k = pos < bytes.Length ? bytes[pos] : 0;
+ var k = pos < bytes.Length ? bytes[pos] : (byte)0;
wr.Write(hex[k >> 4]);
wr.Write(hex[k & 0xf]);
}
@@ -571,7 +571,7 @@ namespace Microsoft.Boogie.SMTLib wr.Write("#b");
for (var pos = node.Type.BvBits - 1; pos >= 0; pos--) {
var i = pos >> 3;
- var k = i < bytes.Length ? bytes[i] : 0;
+ var k = i < bytes.Length ? bytes[i] : (byte)0;
wr.Write((k & (1 << (pos & 7))) == 0 ? '0' : '1');
}
}
|