Skip to content

Commit 5d7b206

Browse files
committed
Corral skips Boogie monomorphic check
So we have to set type encoding to monomorphic manually.
1 parent e76c289 commit 5d7b206

File tree

3 files changed

+3
-0
lines changed

3 files changed

+3
-0
lines changed

source/ConcurrentHoudini/Program.cs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -214,6 +214,7 @@ static void Main(string[] args)
214214
CommandLineOptions.Clo.PrintInstrumented = true;
215215
CommandLineOptions.Clo.StratifiedInliningVerbose = 2;
216216
CommandLineOptions.Clo.UseArrayTheory = true;
217+
CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
217218

218219
Program program;
219220
program = BoogieUtil.ReadAndOnlyResolve(inFileName);

source/Driver.cs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -153,6 +153,7 @@ public static void Initialize(Configs config)
153153
CommandLineOptions.Clo.PrintInstrumented = true;
154154
CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Assume;
155155
CommandLineOptions.Clo.StratifiedInliningVerbose = config.verboseMode;
156+
CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
156157

157158
// /noRemoveEmptyBlocks is needed for field refinement. It ensures that
158159
// we get an actual path in the program (so that we can concretize it)

source/ExplainError/program.cs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1157,6 +1157,7 @@ public static bool ParseCommandLine(string clo)
11571157
var help = ParseArgs(oldArgs, out args);
11581158
CommandLineOptions.Install(new CommandLineOptions());
11591159
CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;
1160+
CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
11601161
CommandLineOptions.Clo.Parse(args);
11611162
return !help;
11621163
}

0 commit comments

Comments
 (0)