diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-08-17 07:45:05 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-08-17 07:45:05 -0700 |
| commit | 88aa33c40ee1cde79fc5b51ab2197da89eb1ddd7 (patch) | |
| tree | 27ee6dfffae8f6e3dc38aff651db6e5006114774 /Source/Provers | |
| parent | bbb739908334dd16d72c06e2ca142bdc48c6387c (diff) | |
deleted lazyinlining option 2 and 3
fixed proc copy bounding
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 5 | ||||
| -rw-r--r-- | Source/Provers/Z3/Prover.cs | 6 |
2 files changed, 0 insertions, 11 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index da9e8faa..9b90b12a 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -152,11 +152,6 @@ namespace Microsoft.Boogie.SMTLib options.AddWeakSmtOption("TYPE_CHECK", "true");
options.AddWeakSmtOption("BV_REFLECT", "true");
- if (CommandLineOptions.Clo.LazyInlining == 2) {
- options.AddWeakSmtOption("MACRO_EXPANSION", "true");
- options.AddWeakSmtOption("WARNING", "false");
- }
-
if (options.TimeLimit > 0) {
options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());
options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index 640f98ae..8929e732 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -84,9 +84,6 @@ namespace Microsoft.Boogie.Z3 StringBuilder cmdLineArgsBldr = new StringBuilder();
AppendCmdLineOption(cmdLineArgsBldr, "si");
- if (CommandLineOptions.Clo.LazyInlining == 2)
- AppendCmdLineOption(cmdLineArgsBldr, "nw");
-
if (CommandLineOptions.Clo.z3AtFlag)
AppendCmdLineOption(cmdLineArgsBldr, "@");
@@ -165,9 +162,6 @@ namespace Microsoft.Boogie.Z3 AddOption(result, "BV_REFLECT", "true");
}
- if (CommandLineOptions.Clo.LazyInlining == 2)
- AddOption(result, "MACRO_EXPANSION", "true");
-
foreach (string opt in CommandLineOptions.Clo.Z3Options) {
Contract.Assert(opt != null);
int eq = opt.IndexOf("=");
|