summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/Z3.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
-rw-r--r--Source/Provers/SMTLib/Z3.cs5
1 files changed, 0 insertions, 5 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);