diff options
| -rw-r--r-- | Source/Model/ModelParser.cs | 12 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 4 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 3 |
3 files changed, 10 insertions, 9 deletions
diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs index cf0ea45f..a88e091e 100644 --- a/Source/Model/ModelParser.cs +++ b/Source/Model/ModelParser.cs @@ -169,13 +169,13 @@ namespace Microsoft.Boogie continue; var words = GetFunctionTokens(line); - + /* Console.WriteLine(""); for (int i = 0; i < words.Count; i++) { Console.Write(words[i] + " "); } - +*/ if (words.Count == 0) continue; var lastWord = words[words.Count - 1]; @@ -215,13 +215,13 @@ namespace Microsoft.Boogie fn = currModel.TryGetFunc(funName); for ( ; ; ) { var tuple = GetFunctionTokens(ReadLine()); - + /* Console.WriteLine(""); for (int i = 0; i < tuple.Count; i++) { Console.Write(tuple[i] + " "); } - +*/ if (tuple == null) BadModel("EOF in function table"); if (tuple.Count == 0) continue; string tuple0 = tuple[0] as string; @@ -598,13 +598,13 @@ namespace Microsoft.Boogie continue; var words = GetParsedTokens(line); - + /* Console.WriteLine(""); for (int i = 0; i < words.Count; i++) { Console.Write(words[i] + " "); } - +*/ if (words.Count == 0) continue; var lastToken = words[words.Count - 1]; if (currModel == null) diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 30cabf60..eaa42b38 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -878,11 +878,11 @@ namespace Microsoft.Boogie.SMTLib if (resp.Arguments[i].ToString().Contains("define-fun"))
modelStr += resp.Arguments[i] + "\n";
}
- Console.WriteLine(modelStr);
+ //Console.WriteLine(modelStr);
}
else if (resp.ArgCount == 0 && resp.Name.Contains("->")) {
modelStr = resp.Name;
- Console.WriteLine(modelStr);
+ //Console.WriteLine(modelStr);
}
else {
HandleProverError("Unexpected prover response getting model: " + resp.ToString());
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 81d5d5d1..04bdc0df 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -274,7 +274,8 @@ namespace Microsoft.Boogie.SMTLib //options.AddWeakSmtOption("MODEL_PARTIAL", "true");
//options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");
- options.AddWeakSmtOption("MODEL_V2", "true");
+ //options.AddWeakSmtOption("MODEL_V2", "true");
+ options.AddWeakSmtOption("pp-bv-literals", "false");
options.AddWeakSmtOption("ASYNC_COMMANDS", "false");
if (!options.OptimizeForBv)
|