diff options
| author |  rustanleino <unknown> | 2010-10-12 00:13:50 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-10-12 00:13:50 +0000 |
| commit | 4fc18b2fe45c9a29cb0b8fe93d3102cec9c83194 (patch) | |
| tree | a324eff1a6d8266938943a038450ce4eb790810b /Source/Provers | |
| parent | c830dff64feadac2f6aa8e0f2a7e647bf3d690f1 (diff) | |
Boogie:
* enhanced the printing of captured states
* addressed some warnings issued by VS 2010
* some code formatting
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/Simplify/ProverInterface.cs | 4 | ||||
| -rw-r--r-- | Source/Provers/Z3/Prover.cs | 7 | ||||
| -rw-r--r-- | Source/Provers/Z3/ProverInterface.cs | 4 |
3 files changed, 8 insertions, 7 deletions
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs index 1f563c0f..1d7bdbb3 100644 --- a/Source/Provers/Simplify/ProverInterface.cs +++ b/Source/Provers/Simplify/ProverInterface.cs @@ -757,6 +757,10 @@ namespace Microsoft.Boogie.Simplify { //Contract.Requires(var != null);
Contract.Ensures(Contract.Result<string>() != null);
+ VCExprVar v = AxBuilder.TryTyped2Untyped(var);
+ if (v != null) {
+ var = v;
+ }
return Namer.Lookup(var);
}
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index 4a16e6b6..33e622ba 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -597,13 +597,6 @@ namespace Microsoft.Boogie.Z3 int k = s.IndexOfAny(new char[] { ' ', '}' }, j);
Contract.Assume(j <= k);
string id = s.Substring(j, k - j);
-#if IS_THIS_A_GOOD_IDEA
- // remove any @@-suffix
- int doubleAt = id.IndexOf("@@");
- if (doubleAt != -1) {
- id = id.Substring(0, doubleAt);
- }
-#endif
j = k + 1;
Contract.Assume(!identifierToPartition.ContainsKey(id)); // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class
identifierToPartition.Add(id, zID);
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs index 9289b5b7..af9668d4 100644 --- a/Source/Provers/Z3/ProverInterface.cs +++ b/Source/Provers/Z3/ProverInterface.cs @@ -295,6 +295,10 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P. //Contract.Requires(var != null);
Contract.Ensures(Contract.Result<string>() != null);
+ VCExprVar v = AxBuilder.TryTyped2Untyped(var);
+ if (v != null) {
+ var = v;
+ }
return Namer.Lookup(var);
}
|