diff options
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 6 | ||||
-rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 10 |
2 files changed, 14 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 4cec5ad4..563dec8f 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -512,9 +512,11 @@ namespace Microsoft.Boogie.SMTLib }
public bool VisitSelectOp(VCExprNAry node, LineariserOptions options)
- {
+ {
var name = SimplifyLikeExprLineariser.SelectOpName(node);
name = ExprLineariser.Namer.GetQuotedName(name, name);
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ name = "select";
WriteApplication(name, node, options);
return true;
}
@@ -523,6 +525,8 @@ namespace Microsoft.Boogie.SMTLib {
var name = SimplifyLikeExprLineariser.StoreOpName(node);
name = ExprLineariser.Namer.GetQuotedName(name, name);
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ name = "store";
WriteApplication(name, node, options);
return true;
}
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 0a03e4ab..b98378b2 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -196,6 +196,10 @@ void ObjectInvariant() private void RegisterSelect(VCExprNAry node)
{
RegisterType(node[0].Type);
+
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ return;
+
string name = SimplifyLikeExprLineariser.SelectOpName(node);
name = Namer.GetQuotedName(name, name);
@@ -209,6 +213,10 @@ void ObjectInvariant() private void RegisterStore(VCExprNAry node)
{
RegisterType(node.Type); // this is the map type, registering it should register also the index and value types
+
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ return;
+
string name = SimplifyLikeExprLineariser.StoreOpName(node);
name = Namer.GetQuotedName(name, name);
@@ -216,7 +224,7 @@ void ObjectInvariant() string decl = "(declare-fun " + name + " (" + node.MapConcat(n => TypeToString(n.Type), " ") + ") " + TypeToString(node.Type) + ")";
AddDeclaration(decl);
- if (CommandLineOptions.Clo.MonomorphicArrays && !CommandLineOptions.Clo.UseArrayTheory) {
+ if (CommandLineOptions.Clo.MonomorphicArrays) {
var sel = SimplifyLikeExprLineariser.SelectOpName(node);
sel = Namer.GetQuotedName(sel, sel);
|