diff options
| author |  qadeer <unknown> | 2010-04-19 01:38:53 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-04-19 01:38:53 +0000 |
| commit | d522d8078db3adfdf41f201bb38f105a7c0bbab1 (patch) | |
| tree | e469f2b7ed332007fe1ad3ecd7014c8e845b6a60 | |
| parent | d03242f9efa515d848f9166244bfaaa9fefd22b0 (diff) | |
Fixed a bug. Call RegisterType before the collection of Select and Store functions in TypeDeclCollector.
| -rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.ssc | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Source/Provers/Z3/TypeDeclCollector.ssc b/Source/Provers/Z3/TypeDeclCollector.ssc index a45ca206..4d6accaf 100644 --- a/Source/Provers/Z3/TypeDeclCollector.ssc +++ b/Source/Provers/Z3/TypeDeclCollector.ssc @@ -182,6 +182,10 @@ namespace Microsoft.Boogie.Z3 //
} else if (node.Op is VCExprStoreOp) {
//
+ RegisterType(node[0].Type);
+ RegisterType(node[1].Type);
+ RegisterType(node[2].Type);
+ RegisterType(node.Type);
string name = SimplifyLikeExprLineariser.StoreOpName(node);
if (!KnownStoreFunctions.ContainsKey(name)) {
AddDeclaration("(DEFOP " + name +
@@ -195,6 +199,9 @@ namespace Microsoft.Boogie.Z3 //
} else if (node.Op is VCExprSelectOp) {
//
+ RegisterType(node[0].Type);
+ RegisterType(node[1].Type);
+ RegisterType(node.Type);
string name = SimplifyLikeExprLineariser.SelectOpName(node);
if (!KnownSelectFunctions.ContainsKey(name)) {
AddDeclaration("(DEFOP " + name +
|