diff options
| author |  akashlal <unknown> | 2013-04-18 22:29:51 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2013-04-18 22:29:51 +0530 |
| commit | 2afe289c11d78711d4483e1ed36346998689668c (patch) | |
| tree | 2d09536f42cfcd000aeeeeef00b8365ae1ef0928 /Source/BoogieDriver/BoogieDriver.cs | |
| parent | a2fcc9e7617800e2139a9cbbfa720222e4c1b6f5 (diff) | |
AbsHoudini: Added support for /inlineDepth, and fixed the regression tests
(all pass)
Diffstat (limited to 'Source/BoogieDriver/BoogieDriver.cs')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 9b31c31e..9ef365c0 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -640,6 +640,8 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.AbstractHoudini != null)
{
//CommandLineOptions.Clo.PrintErrorModel = 1;
+ CommandLineOptions.Clo.UseProverEvaluate = true;
+ CommandLineOptions.Clo.ModelViewFile = "z3model";
CommandLineOptions.Clo.UseArrayTheory = true;
CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
CommandLineOptions.Clo.ProverCCLimit = 1;
|