diff options
| -rw-r--r-- | Source/Provers/Z3api/ContextLayer.cs | 336 | ||||
| -rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 9 | ||||
| -rw-r--r-- | Source/Provers/Z3api/TypeAdapter.cs | 34 | ||||
| -rw-r--r-- | Source/Provers/Z3api/VCExprVisitor.cs | 150 | ||||
| -rw-r--r-- | Source/Provers/Z3api/Z3api.csproj | 8 | ||||
| -rw-r--r-- | Test/z3api/Answer | 174 | ||||
| -rw-r--r-- | Test/z3api/bar1.bpl | 26 | ||||
| -rw-r--r-- | Test/z3api/bar2.bpl | 24 | ||||
| -rw-r--r-- | Test/z3api/bar3.bpl | 41 | ||||
| -rw-r--r-- | Test/z3api/bar4.bpl | 38 | ||||
| -rw-r--r-- | Test/z3api/bar6.bpl | 36 | ||||
| -rw-r--r-- | Test/z3api/boog35.bpl | 17 | ||||
| -rw-r--r-- | Test/z3api/runtest.bat | 13 |
13 files changed, 501 insertions, 405 deletions
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index ed45c4fc..390d875d 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -11,6 +11,9 @@ using Microsoft.Z3; using Microsoft.Boogie.VCExprAST;
using Microsoft.Basetypes;
+using Z3Model = Microsoft.Z3.Model;
+using BoogieModel = Microsoft.Boogie.Model;
+
namespace Microsoft.Boogie.Z3
{
public class Z3Config
@@ -20,21 +23,6 @@ namespace Microsoft.Boogie.Z3 private string logFilename;
private List<string> debugTraces = new List<string>();
- public void SetModel(bool enabled)
- {
- config.SetParamValue("MODEL", (enabled ? "true" : "false"));
- }
-
- public void SetSoftTimeout(string timeout)
- {
- config.SetParamValue("SOFT_TIMEOUT", timeout);
- }
-
- public void SetTypeCheck(bool enabled)
- {
- config.SetParamValue("TYPE_CHECK", (enabled ? "true" : "false"));
- }
-
public void SetCounterExample(int counterexample)
{
this.counterexamples = counterexample;
@@ -69,102 +57,6 @@ namespace Microsoft.Boogie.Z3 }
}
- internal class PartitionMap
- {
- private Context ctx;
- private Model model;
- private Dictionary<Term, int> termToPartition = new Dictionary<Term, int>();
- private Dictionary<object, int> valueToPartition = new Dictionary<object, int>();
- private List<Object> partitionToValue = new List<Object>();
- private int partitionCounter = 0;
- public int PartitionCounter { get { return partitionCounter; } }
-
- public PartitionMap(Context ctx, Model z3Model)
- {
- this.ctx = ctx;
- this.model = z3Model;
- }
-
- public int GetPartition(Term value)
- {
- int result;
- if (!termToPartition.TryGetValue(value, out result))
- {
- result = partitionCounter++;
- termToPartition.Add(value, result);
- partitionToValue.Add(null);
- object constant = Evaluate(value);
- valueToPartition.Add(constant, result);
- partitionToValue[result] = constant;
- }
- return result;
- }
-
- private object Evaluate(Term v)
- {
- Sort s = v.GetSort();
- Sort boolSort = ctx.MkBoolSort();
- Sort intSort = ctx.MkIntSort();
- ArrayValue av;
-
- if (s.Equals(boolSort))
- {
- return ctx.GetBoolValue(v);
- }
- else if (s.Equals(intSort)) {
- int i;
- long il;
- uint u;
- ulong ul;
- if (ctx.TryGetNumeralInt(v, out i)) {
- return BigNum.FromInt(i);
- }
- else if (ctx.TryGetNumeralInt64(v, out il)) {
- return BigNum.FromLong(il);
- }
- else if (ctx.TryGetNumeralUInt(v, out u)) {
- return BigNum.FromUInt(u);
- }
- else if (ctx.TryGetNumeralUInt64(v, out ul)) {
- return BigNum.FromULong(ul);
- }
- else {
- string str = v.ToString();
- return GetPartition(v);
- //return BigNum.FromString(ctx.GetNumeralString(v));
- }
- }
- else if (model.TryGetArrayValue(v, out av)) {
- List<List<int>> arrayValue = new List<List<int>>();
- List<int> tuple;
- for (int i = 0; i < av.Domain.Length; i++) {
- tuple = new List<int>();
- tuple.Add(GetPartition(av.Domain[i]));
- tuple.Add(GetPartition(av.Range[i]));
- arrayValue.Add(tuple);
- }
- tuple = new List<int>();
- tuple.Add(GetPartition(av.ElseCase));
- arrayValue.Add(tuple);
- return arrayValue;
- }
- else {
- // The term is uninterpreted; just return the partition id.
- return GetPartition(v);
- }
- }
-
- public List<Object> PartitionToValue(Context ctx)
- {
- return partitionToValue;
- }
-
- public Dictionary<object, int> ValueToPartition(Context ctx)
- {
- return valueToPartition;
- }
- }
-
internal class BacktrackDictionary<K, V>
{
private Dictionary<K, V> dictionary = new Dictionary<K, V>();
@@ -217,86 +109,11 @@ namespace Microsoft.Boogie.Z3 }
}
- internal class BoogieErrorModelBuilder
- {
- private Z3Context container;
- private PartitionMap partitionMap;
-
- public BoogieErrorModelBuilder(Z3Context container, Model z3Model)
- {
- this.container = container;
- this.partitionMap = new PartitionMap(((Z3Context)container).z3, z3Model);
- }
-
- private Dictionary<string, int> CreateConstantToPartition(Model z3Model)
- {
- Dictionary<string, int> constantToPartition = new Dictionary<string, int>();
- foreach (FuncDecl c in z3Model.GetModelConstants())
- {
- string name = container.GetDeclName(c);
- int pid = partitionMap.GetPartition(z3Model.Eval(c, new Term[0]));
- constantToPartition.Add(name, pid);
- }
- return constantToPartition;
- }
-
- private List<List<string>> CreatePartitionToConstant(Dictionary<string, int> constantToPartition)
- {
- List<List<string>> partitionToConstant = new List<List<string>>();
- for (int i = 0; i < partitionMap.PartitionCounter; i++)
- {
- partitionToConstant.Add(new List<string>());
- }
- foreach (string s in constantToPartition.Keys)
- {
- partitionToConstant[constantToPartition[s]].Add(s);
- }
- return partitionToConstant;
- }
-
- private Dictionary<string, List<List<int>>> CreateFunctionToPartition(Model z3Model)
- {
- Dictionary<string, List<List<int>>> functionToPartition = new Dictionary<string, List<List<int>>>();
-
- foreach (KeyValuePair<FuncDecl, FunctionGraph> kv in z3Model.GetFunctionGraphs())
- {
- List<List<int>> f_tuples = new List<List<int>>();
- string f_name = container.GetDeclName(kv.Key);
- FunctionGraph graph = kv.Value;
- foreach (FunctionEntry entry in graph.Entries)
- {
- List<int> tuple = new List<int>();
- foreach (Term v in entry.Arguments)
- {
- tuple.Add(partitionMap.GetPartition(z3Model.Eval(v)));
- }
- tuple.Add(partitionMap.GetPartition(z3Model.Eval(entry.Result)));
- f_tuples.Add(tuple);
- }
- List<int> else_tuple = new List<int>();
- else_tuple.Add(partitionMap.GetPartition(z3Model.Eval(graph.Else)));
- f_tuples.Add(else_tuple);
- functionToPartition.Add(f_name, f_tuples);
- }
- return functionToPartition;
- }
-
- public Z3ErrorModel BuildBoogieModel(Model z3Model)
- {
- Dictionary<string, int> constantToPartition = CreateConstantToPartition(z3Model);
- Dictionary<string, List<List<int>>> functionToPartition = CreateFunctionToPartition(z3Model);
- List<List<string>> partitionToConstant = CreatePartitionToConstant(constantToPartition);
- List<Object> partitionToValue = partitionMap.PartitionToValue(((Z3Context)container).z3);
- Dictionary<object, int> valueToPartition = partitionMap.ValueToPartition(((Z3Context)container).z3);
- return new Z3ErrorModel(constantToPartition, partitionToConstant, partitionToValue, valueToPartition, functionToPartition);
- }
- }
-
public class Z3ErrorModelAndLabels
{
- private Z3ErrorModel _errorModel;
+ private ErrorModel _errorModel;
private List<string> _relevantLabels;
- public Z3ErrorModel ErrorModel
+ public ErrorModel ErrorModel
{
get { return this._errorModel; }
}
@@ -304,7 +121,7 @@ namespace Microsoft.Boogie.Z3 {
get { return this._relevantLabels; }
}
- public Z3ErrorModelAndLabels(Z3ErrorModel errorModel, List<string> relevantLabels)
+ public Z3ErrorModelAndLabels(ErrorModel errorModel, List<string> relevantLabels)
{
this._errorModel = errorModel;
this._relevantLabels = relevantLabels;
@@ -461,12 +278,13 @@ namespace Microsoft.Boogie.Z3 return true;
}
- private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List<string> relevantLabels) {
+ /*
+ private Z3ErrorModelAndLabels BuildZ3ErrorModel(Z3Model z3Model, List<string> relevantLabels) {
BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this, z3Model);
Z3ErrorModel boogieModel = boogieErrorBuilder.BuildBoogieModel(z3Model);
return new Z3ErrorModelAndLabels(boogieModel, new List<string>(relevantLabels));
}
-
+ */
private void DisplayRelevantLabels(List<string> relevantLabels) {
foreach (string labelName in relevantLabels) {
System.Console.Write(labelName + ",");
@@ -480,8 +298,9 @@ namespace Microsoft.Boogie.Z3 LBool outcome = LBool.Undef;
Debug.Assert(0 < this.config.Counterexamples);
while (true) {
- Model z3Model;
+ Z3Model z3Model;
outcome = z3.CheckAndGetModel(out z3Model);
+
log("(check-sat)");
if (outcome == LBool.False)
break;
@@ -505,13 +324,27 @@ namespace Microsoft.Boogie.Z3 }
labelStrings.Add(labelName);
}
- boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));
+
+ var sw = new StringWriter();
+ sw.WriteLine("*** MODEL");
+ z3Model.Display(sw);
+ sw.WriteLine("*** END_MODEL");
+ var sr = new StringReader(sw.ToString());
+ var models = Microsoft.Boogie.Model.ParseModels(sr);
+
+
+ Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List<string>(labelStrings));
+
+
+ boogieErrors.Add(e);
if (boogieErrors.Count < this.config.Counterexamples) {
z3.BlockLiterals(labels);
log("block-literals {0}", labels);
}
+
+
labels.Dispose();
z3Model.Dispose();
if (boogieErrors.Count == this.config.Counterexamples)
@@ -538,7 +371,7 @@ namespace Microsoft.Boogie.Z3 unsatCore = new List<int>();
LBool outcome = LBool.Undef;
- Model z3Model;
+ Z3Model z3Model;
Term proof;
Term[] core;
Term[] assumption_terms = new Term[assumptions.Count];
@@ -568,7 +401,16 @@ namespace Microsoft.Boogie.Z3 }
labelStrings.Add(labelName);
}
- boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));
+
+ var sw = new StringWriter();
+ sw.WriteLine("*** MODEL");
+ z3Model.Display(sw);
+ sw.WriteLine("*** END_MODEL");
+ var sr = new StringReader(sw.ToString());
+ var models = Microsoft.Boogie.Model.ParseModels(sr);
+
+ Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List<string>(labelStrings));
+ boogieErrors.Add(e);
labels.Dispose();
z3Model.Dispose();
@@ -668,37 +510,83 @@ namespace Microsoft.Boogie.Z3 return safeLiterals;
}
- public Term Make(string op, List<Term> children) {
+ public Term Make(VCExprOp op, List<Term> children) {
Term[] unwrapChildren = children.ToArray();
- Term term;
- switch (op) {
- // formulas
- case "AND": term = z3.MkAnd(unwrapChildren); break;
- case "OR": term = z3.MkOr(unwrapChildren); break;
- case "IMPLIES": term = z3.MkImplies(unwrapChildren[0], unwrapChildren[1]); break;
- case "NOT": term = z3.MkNot(unwrapChildren[0]); break;
- case "IFF": term = z3.MkIff(unwrapChildren[0], unwrapChildren[1]); break;
- // terms
- case "EQ": term = z3.MkEq(unwrapChildren[0], unwrapChildren[1]); break;
- case "NEQ": term = z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1])); break;
- case "DISTINCT": term = z3.MkDistinct(unwrapChildren); break;
- // terms
- case "<": term = z3.MkLt(unwrapChildren[0], unwrapChildren[1]); break;
- case ">": term = z3.MkGt(unwrapChildren[0], unwrapChildren[1]); break;
- case "<=": term = z3.MkLe(unwrapChildren[0], unwrapChildren[1]); break;
- case ">=": term = z3.MkGe(unwrapChildren[0], unwrapChildren[1]); break;
- case "+": term = z3.MkAdd(unwrapChildren); break;
- case "-": term = z3.MkSub(unwrapChildren); break;
- case "/": term = z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); break;
- case "%": term = z3.MkMod(unwrapChildren[0], unwrapChildren[1]); break;
- case "*": term = z3.MkMul(unwrapChildren); break;
- default: {
- FuncDecl f = GetFunction(op);
- term = z3.MkApp(f, unwrapChildren);
- }
- break;
+ VCExprBoogieFunctionOp boogieFunctionOp = op as VCExprBoogieFunctionOp;
+ if (boogieFunctionOp != null) {
+ FuncDecl f = GetFunction(boogieFunctionOp.Func.Name);
+ return z3.MkApp(f, unwrapChildren);
+ }
+ VCExprDistinctOp distinctOp = op as VCExprDistinctOp;
+ if (distinctOp != null) {
+ return z3.MkDistinct(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.AndOp) {
+ return z3.MkAnd(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.OrOp) {
+ return z3.MkOr(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.ImpliesOp) {
+ return z3.MkImplies(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.NotOp) {
+ return z3.MkNot(unwrapChildren[0]);
+ }
+
+ if (op == VCExpressionGenerator.EqOp) {
+ return z3.MkEq(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.NeqOp) {
+ return z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1]));
+ }
+
+ if (op == VCExpressionGenerator.LtOp) {
+ return z3.MkLt(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.LeOp) {
+ return z3.MkLe(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.GtOp) {
+ return z3.MkGt(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.GeOp) {
+ return z3.MkGe(unwrapChildren[0], unwrapChildren[1]);
}
- return term;
+
+ if (op == VCExpressionGenerator.AddOp) {
+ return z3.MkAdd(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.SubOp) {
+ return z3.MkSub(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.DivOp) {
+ return z3.MkDiv(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.MulOp) {
+ return z3.MkMul(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.ModOp) {
+ return z3.MkMod(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.IfThenElseOp) {
+ return z3.MkIte(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]);
+ }
+
+ throw new Exception("unhandled boogie operator");
}
}
}
\ No newline at end of file diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index f691cffc..39acc5db 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -202,7 +202,10 @@ namespace Microsoft.Boogie.Z3 private static Z3Config BuildConfig(int timeout, bool nativeBv)
{
Z3Config config = new Z3Config();
- config.SetModel(true);
+ config.Config.SetParamValue("MODEL", "true");
+ config.Config.SetParamValue("MODEL_V2", "true");
+ config.Config.SetParamValue("MODEL_COMPLETION", "true");
+ config.Config.SetParamValue("MBQI", "false");
if (0 <= CommandLineOptions.Clo.ProverCCLimit)
{
@@ -211,7 +214,7 @@ namespace Microsoft.Boogie.Z3 if (0 <= timeout)
{
- config.SetSoftTimeout(timeout.ToString());
+ config.Config.SetParamValue("SOFT_TIMEOUT", timeout.ToString());
}
if (CommandLineOptions.Clo.SimplifyLogFilePath != null)
@@ -219,7 +222,7 @@ namespace Microsoft.Boogie.Z3 config.SetLogFilename(CommandLineOptions.Clo.SimplifyLogFilePath);
}
- config.SetTypeCheck(true);
+ config.Config.SetParamValue("TYPE_CHECK", "true");
return config;
}
diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index de5ebd8f..b0dd1eb4 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -87,21 +87,17 @@ namespace Microsoft.Boogie.Z3 this.container = context;
}
- private Sort GetMapType(MapType mapType)
- {
- Context z3 = ((Z3Context)container).z3;
- if (!mapTypes.ContainsKey(mapType))
- {
- Debug.Assert(mapType.Arguments.Length == 1, "Z3api only supports maps of arity 1");
- Sort domain = GetType(mapType.Arguments[0]);
- Sort range = GetType(mapType.Result);
- Sort typeAst = BuildMapType(domain, range);
- mapTypes.Add(mapType, typeAst);
+ private Sort GetMapType(MapType mapType) {
+ Context z3 = ((Z3Context)container).z3;
+ if (!mapTypes.ContainsKey(mapType)) {
+ Type result = mapType.Result;
+ for (int i = mapType.Arguments.Length-1; i > 0; i--) {
+ GetType(result);
+ result = new MapType(mapType.tok, new TypeVariableSeq(), new TypeSeq(mapType.Arguments[i]), result);
}
- Sort result;
- bool containsKey = mapTypes.TryGetValue(mapType, out result);
- Debug.Assert(containsKey);
- return result;
+ mapTypes.Add(mapType, BuildMapType(GetType(mapType.Arguments[0]), GetType(result)));
+ }
+ return mapTypes[mapType];
}
private Sort GetBvType(BvType bvType)
@@ -158,15 +154,13 @@ namespace Microsoft.Boogie.Z3 public Sort BuildMapType(Sort domain, Sort range)
{
Context z3 = ((Z3Context)container).z3;
- Sort typeAst = z3.MkArraySort(domain, range);
- return typeAst;
+ return z3.MkArraySort(domain, range);
}
public Sort BuildBvType(BvType bvType)
{
Context z3 = ((Z3Context)container).z3;
- Sort typeAst = z3.MkBvSort((uint)bvType.Bits);
- return typeAst;
+ return z3.MkBvSort((uint)bvType.Bits);
}
public Sort BuildBasicType(BasicType basicType)
@@ -188,11 +182,9 @@ namespace Microsoft.Boogie.Z3 public Sort BuildCtorType(CtorType ctorType) {
Context z3 = ((Z3Context)container).z3;
- Sort typeAst;
if (ctorType.Arguments.Length > 0)
throw new Exception("Type constructor of non-zero arity are not handled");
- typeAst = z3.MkSort(ctorType.Decl.Name);
- return typeAst;
+ return z3.MkSort(ctorType.Decl.Name);
}
}
}
\ No newline at end of file diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs index aa47d7e0..bf6dab94 100644 --- a/Source/Provers/Z3api/VCExprVisitor.cs +++ b/Source/Provers/Z3api/VCExprVisitor.cs @@ -17,15 +17,15 @@ namespace Microsoft.Boogie.Z3 {
public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions>
{
- private Z3apiOpLineariser OpLinObject = null;
+ private Z3apiOpLineariser opLineariser = null;
private IVCExprOpVisitor<Term, LineariserOptions> OpLineariser
{
get
{
Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>() != null);
- if (OpLinObject == null)
- OpLinObject = new Z3apiOpLineariser(this);
- return OpLinObject;
+ if (opLineariser == null)
+ opLineariser = new Z3apiOpLineariser(this);
+ return opLineariser;
}
}
@@ -91,7 +91,7 @@ namespace Microsoft.Boogie.Z3 }
}
- return cm.Make(opString, asts);
+ return cm.Make(op, asts);
}
return node.Accept<Term, LineariserOptions>(OpLineariser, options);
@@ -246,7 +246,7 @@ namespace Microsoft.Boogie.Z3 ///////////////////////////////////////////////////////////////////////////////////
- private Term WriteApplication(string op, IEnumerable<VCExpr> terms, LineariserOptions options)
+ private Term WriteApplication(VCExprOp op, IEnumerable<VCExpr> terms, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(op != null);
@@ -267,76 +267,49 @@ namespace Microsoft.Boogie.Z3 {
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("NOT", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitEqOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("EQ", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitNeqOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("NEQ", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitAndOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("AND", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitOrOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("OR", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- if (options.InverseImplies)
- {
- List<Term> args = new List<Term>();
-
- args.Add(ExprLineariser.Linearise(node[1], options));
- List<Term> t = new List<Term>();
- t.Add(ExprLineariser.Linearise(node[0], options));
- args.Add(ExprLineariser.cm.Make("NOT", t));
- return ExprLineariser.cm.Make("OR", args);
- }
- else
- {
- return WriteApplication("IMPLIES", node, options);
- }
+ return WriteApplication(node.Op, node, options);
}
- public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options)
{
- Contract.Requires(options != null);
- Contract.Requires(node != null);
-
- if (node.Length < 2)
- {
- return ExprLineariser.Linearise(VCExpressionGenerator.True, options);
- }
- else
- {
- List<Term> args = new List<Term>();
- foreach (VCExpr e in node)
- {
- Contract.Assert(e != null);
- args.Add(ExprLineariser.Linearise(e, options));
- }
- return ExprLineariser.cm.Make("DISTINCT", args);
- }
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitLabelOp(VCExprNAry node, LineariserOptions options)
@@ -358,10 +331,24 @@ namespace Microsoft.Boogie.Z3 Contract.Assert(e != null);
args.Add(ExprLineariser.Linearise(e, options));
}
+ System.Diagnostics.Debug.Assert(args.Count >= 2);
- Term[] unwrapChildren = args.ToArray();
- return ExprLineariser.cm.z3.MkArraySelect(unwrapChildren[0], unwrapChildren[1]);
- // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.SelectOpName(node), args);
+ Term selectTerm = args[0];
+ for (int i = 1; i < args.Count; i++) {
+ selectTerm = ExprLineariser.cm.z3.MkArraySelect(selectTerm, args[i]);
+ }
+ return selectTerm;
+ }
+
+ private Term ConstructStoreTerm(Term mapTerm, List<Term> args, int index) {
+ System.Diagnostics.Debug.Assert(0 < index && index < args.Count - 1);
+ if (index == args.Count - 2) {
+ return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], args[index + 1]);
+ }
+ else {
+ Term t = ConstructStoreTerm(ExprLineariser.cm.z3.MkArraySelect(mapTerm, args[index]), args, index + 1);
+ return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], t);
+ }
}
public Term VisitStoreOp(VCExprNAry node, LineariserOptions options)
@@ -374,10 +361,7 @@ namespace Microsoft.Boogie.Z3 Contract.Assert(e != null);
args.Add(ExprLineariser.Linearise(e, options));
}
-
- Term[] unwrapChildren = args.ToArray();
- return ExprLineariser.cm.z3.MkArrayStore(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]);
- // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.StoreOpName(node), args);
+ return ConstructStoreTerm(args[0], args, 1);
}
public Term VisitBvOp(VCExprNAry node, LineariserOptions options)
@@ -431,129 +415,97 @@ namespace Microsoft.Boogie.Z3 {
Contract.Requires(options != null);
Contract.Requires(node != null);
-
- List<Term> args = new List<Term>();
- args.Add(ExprLineariser.Linearise(node[0], options));
- args.Add(ExprLineariser.Linearise(node[1], options));
- args.Add(ExprLineariser.Linearise(node[2], options));
- return ExprLineariser.cm.Make("ITE", args);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitCustomOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(node != null);
Contract.Requires(options != null);
- VCExprCustomOp op = (VCExprCustomOp)node.Op;
- List<Term> args = new List<Term>();
- foreach (VCExpr arg in node)
- {
- args.Add(ExprLineariser.Linearise(arg, options));
- }
- return ExprLineariser.cm.Make(op.Name, args);
+ return WriteApplication(node.Op, node, options);
}
- public Term VisitAddOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- if (CommandLineOptions.Clo.ReflectAdd)
- {
- return WriteApplication("Reflect$Add", node, options);
- }
- else
- {
- return WriteApplication("+", node, options);
- }
+ public Term VisitAddOp(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitSubOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("-", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitMulOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("*", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitDivOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("/", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitModOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("%", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitLtOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("<", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitLeOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("<=", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitGtOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication(">", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitGeOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication(">=", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("<:", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("<::", node, options);
+ return WriteApplication(node.Op, node, options);
}
public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;
- Contract.Assert(op != null);
- string funcName = op.Func.Name;
- Contract.Assert(funcName != null);
- string bvzName = op.Func.FindStringAttribute("external");
- if (bvzName != null) funcName = bvzName;
-
- List<Term> args = new List<Term>();
- foreach (VCExpr e in node)
- {
- Contract.Assert(e != null);
- args.Add(ExprLineariser.Linearise(e, options));
- }
- return ExprLineariser.cm.Make(funcName, args);
+ return WriteApplication(node.Op, node, options);
}
}
}
diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index e02243ce..94184957 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -146,6 +146,14 @@ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
<Name>Core</Name>
</ProjectReference>
+ <ProjectReference Include="..\..\Model\Model.csproj">
+ <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
+ <Name>Model</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\ParserHelper\ParserHelper.csproj">
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
+ <Name>ParserHelper</Name>
+ </ProjectReference>
<ProjectReference Include="..\..\VCExpr\VCExpr.csproj">
<Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
<Name>VCExpr</Name>
diff --git a/Test/z3api/Answer b/Test/z3api/Answer index 782aa852..d18f12ef 100644 --- a/Test/z3api/Answer +++ b/Test/z3api/Answer @@ -1,9 +1,9 @@ -------------------- boog0.bpl --------------------
-boog0.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement.
-boog0.bpl(45,3): Related location: This is the postcondition that might not hold.
+boog0.bpl(49,1): Error BP5003: A postcondition might not hold on this return path.
+boog0.bpl(43,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog0.bpl(48,7): anon0
+ boog0.bpl(46,7): anon0
Boogie program verifier finished with 1 verified, 1 error
@@ -12,17 +12,17 @@ Boogie program verifier finished with 1 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog2.bpl --------------------
-boog2.bpl(23,1): Error BP5003: A postcondition might not hold at this return statement.
-boog2.bpl(19,3): Related location: This is the postcondition that might not hold.
+boog2.bpl(24,1): Error BP5003: A postcondition might not hold on this return path.
+boog2.bpl(20,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog2.bpl(22,8): anon0
+ boog2.bpl(23,8): anon0
Boogie program verifier finished with 1 verified, 1 error
-------------------- boog3.bpl --------------------
-boog3.bpl(6,3): Error BP5001: This assertion might not hold.
+boog3.bpl(7,3): Error BP5001: This assertion might not hold.
Execution trace:
- boog3.bpl(6,3): anon0
+ boog3.bpl(7,3): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -31,11 +31,11 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog5.bpl --------------------
-boog5.bpl(36,3): Error BP5003: A postcondition might not hold at this return statement.
-boog5.bpl(29,3): Related location: This is the postcondition that might not hold.
+boog5.bpl(37,3): Error BP5003: A postcondition might not hold on this return path.
+boog5.bpl(30,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog5.bpl(32,3): anon0
- boog5.bpl(35,13): anon3_Else
+ boog5.bpl(33,3): anon0
+ boog5.bpl(36,13): anon3_Else
Boogie program verifier finished with 0 verified, 1 error
@@ -44,91 +44,92 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog7.bpl --------------------
-boog7.bpl(17,1): Error BP5003: A postcondition might not hold at this return statement.
-boog7.bpl(13,3): Related location: This is the postcondition that might not hold.
+boog7.bpl(18,1): Error BP5003: A postcondition might not hold on this return path.
+boog7.bpl(14,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog7.bpl(16,11): anon0
+ boog7.bpl(17,11): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog8.bpl --------------------
-boog8.bpl(7,12): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
-boog8.bpl(7,18): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
-2 type checking errors detected in boog8.bpl
+boog8.bpl(23,1): Error BP5003: A postcondition might not hold on this return path.
+boog8.bpl(19,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog8.bpl(22,11): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
-------------------- boog9.bpl --------------------
-boog9.bpl(19,1): Error BP5003: A postcondition might not hold at this return statement.
-boog9.bpl(15,3): Related location: This is the postcondition that might not hold.
+boog9.bpl(20,1): Error BP5003: A postcondition might not hold on this return path.
+boog9.bpl(16,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog9.bpl(18,11): anon0
+ boog9.bpl(19,11): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog10.bpl --------------------
-boog10.bpl(18,3): Error BP5001: This assertion might not hold.
+boog10.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- boog10.bpl(18,3): anon0
+ boog10.bpl(19,3): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog11.bpl --------------------
-boog11.bpl(14,1): Error BP5003: A postcondition might not hold at this return statement.
-boog11.bpl(10,3): Related location: This is the postcondition that might not hold.
+boog11.bpl(15,1): Error BP5003: A postcondition might not hold on this return path.
+boog11.bpl(11,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog11.bpl(13,8): anon0
+ boog11.bpl(14,8): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog12.bpl --------------------
-boog12.bpl(18,1): Error BP5003: A postcondition might not hold at this return statement.
-boog12.bpl(13,3): Related location: This is the postcondition that might not hold.
+boog12.bpl(19,1): Error BP5003: A postcondition might not hold on this return path.
+boog12.bpl(14,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog12.bpl(16,16): anon0
+ boog12.bpl(17,16): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog13.bpl --------------------
-boog13.bpl(9,11): Error: more than one declaration of variable name: v
+boog13.bpl(10,18): Error: more than one declaration of variable name: v
1 name resolution errors detected in boog13.bpl
-------------------- boog14.bpl --------------------
-boog14.bpl(11,1): Error BP5003: A postcondition might not hold at this return statement.
-boog14.bpl(8,1): Related location: This is the postcondition that might not hold.
+boog14.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+boog14.bpl(9,1): Related location: This is the postcondition that might not hold.
Execution trace:
- boog14.bpl(10,8): anon0
+ boog14.bpl(11,8): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog15.bpl --------------------
-boog15.bpl(10,1): Error BP5003: A postcondition might not hold at this return statement.
-boog15.bpl(7,1): Related location: This is the postcondition that might not hold.
+boog15.bpl(11,1): Error BP5003: A postcondition might not hold on this return path.
+boog15.bpl(8,1): Related location: This is the postcondition that might not hold.
Execution trace:
- boog15.bpl(9,8): anon0
+ boog15.bpl(10,8): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog16.bpl --------------------
-boog16.bpl(11,1): Error BP5003: A postcondition might not hold at this return statement.
-boog16.bpl(8,1): Related location: This is the postcondition that might not hold.
+boog16.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+boog16.bpl(9,1): Related location: This is the postcondition that might not hold.
Execution trace:
- boog16.bpl(10,8): anon0
+ boog16.bpl(11,8): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog17.bpl --------------------
-boog17.bpl(24,3): Error BP5001: This assertion might not hold.
+boog17.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- boog17.bpl(15,1): start
- boog17.bpl(19,1): label_3
- boog17.bpl(22,1): label_4
+ boog17.bpl(17,1): start
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog18.bpl --------------------
-boog18.bpl(15,1): Error BP5003: A postcondition might not hold at this return statement.
-boog18.bpl(12,1): Related location: This is the postcondition that might not hold.
+boog18.bpl(16,1): Error BP5003: A postcondition might not hold on this return path.
+boog18.bpl(13,1): Related location: This is the postcondition that might not hold.
Execution trace:
- boog18.bpl(14,4): anon0
+ boog18.bpl(15,4): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -137,9 +138,9 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog20.bpl --------------------
-boog20.bpl(15,1): Error BP5001: This assertion might not hold.
+boog20.bpl(16,1): Error BP5001: This assertion might not hold.
Execution trace:
- boog20.bpl(15,1): anon0
+ boog20.bpl(16,1): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -148,7 +149,7 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog22.bpl --------------------
-boog22.bpl(4,9): Error: more than one declaration of function/procedure name: f1
+boog22.bpl(5,9): Error: more than one declaration of function/procedure name: f1
1 name resolution errors detected in boog22.bpl
-------------------- boog23.bpl --------------------
@@ -176,12 +177,83 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog31.bpl --------------------
-boog31.bpl(12,1): Error BP5001: This assertion might not hold.
+boog31.bpl(13,1): Error BP5001: This assertion might not hold.
Execution trace:
- boog31.bpl(12,1): anon0
+ boog31.bpl(13,1): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog34.bpl --------------------
Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog35.bpl --------------------
+boog35.bpl(16,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ boog35.bpl(14,11): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+
+-------------------- bar1.bpl --------------------
+bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
+bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ bar1.bpl(24,3): anon0
+ Inlined call to procedure foo begins
+ bar1.bpl(13,5): anon0
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- bar2.bpl --------------------
+bar2.bpl(21,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar2.bpl(19,3): anon0
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(9,7): anon3_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(6,7): anon3_Then
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- bar3.bpl --------------------
+bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
+bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ bar3.bpl(38,3): anon0
+ Inlined call to procedure foo begins
+ bar3.bpl(18,3): anon0
+ bar3.bpl(24,7): anon3_Else
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(10,7): anon3_Else
+ Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(10,7): anon3_Else
+ Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(10,7): anon3_Else
+ Inlined call to procedure bar ends
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- bar4.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- bar6.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/z3api/bar1.bpl b/Test/z3api/bar1.bpl new file mode 100644 index 00000000..845954d5 --- /dev/null +++ b/Test/z3api/bar1.bpl @@ -0,0 +1,26 @@ +var x: int;
+var y: int;
+
+procedure {:inline 1} bar()
+modifies y;
+{
+ y := y + 1;
+}
+
+procedure {:inline 1} foo()
+modifies x, y;
+{
+ x := x + 1;
+ call bar();
+ call bar();
+ x := x + 1;
+}
+
+procedure main()
+requires x == y;
+ensures x != y;
+modifies x, y;
+{
+ call foo();
+}
+
diff --git a/Test/z3api/bar2.bpl b/Test/z3api/bar2.bpl new file mode 100644 index 00000000..76991a8f --- /dev/null +++ b/Test/z3api/bar2.bpl @@ -0,0 +1,24 @@ +
+procedure {:inline 1} foo() returns (x: bool)
+{
+ var b: bool;
+ if (b) {
+ x := false;
+ return;
+ } else {
+ x := true;
+ return;
+ }
+}
+
+procedure main()
+{
+ var b1: bool;
+ var b2: bool;
+
+ call b1 := foo();
+ call b2 := foo();
+ assert b1 == b2;
+}
+
+
diff --git a/Test/z3api/bar3.bpl b/Test/z3api/bar3.bpl new file mode 100644 index 00000000..7bd91184 --- /dev/null +++ b/Test/z3api/bar3.bpl @@ -0,0 +1,41 @@ +var y: int;
+var x: int;
+
+procedure {:inline 1} bar(b: bool)
+modifies y;
+{
+ if (b) {
+ y := y + 1;
+ } else {
+ y := y - 1;
+ }
+}
+
+procedure {:inline 1} foo()
+modifies x, y;
+{
+ var b: bool;
+ if (b) {
+ x := x + 1;
+ call bar(true);
+ call bar(true);
+ x := x + 1;
+ } else {
+ x := x - 1;
+ call bar(false);
+ call bar(false);
+ x := x - 1;
+ }
+}
+
+
+procedure main()
+requires x == y;
+ensures x == y;
+modifies x, y;
+modifies y;
+{
+ call foo();
+ assert x == y;
+ call bar(false);
+}
diff --git a/Test/z3api/bar4.bpl b/Test/z3api/bar4.bpl new file mode 100644 index 00000000..84640811 --- /dev/null +++ b/Test/z3api/bar4.bpl @@ -0,0 +1,38 @@ +var y: int;
+var x: int;
+
+procedure {:inline 1} bar() returns (b: bool)
+modifies y;
+{
+ if (b) {
+ y := y + 1;
+ } else {
+ y := y - 1;
+ }
+}
+
+procedure {:inline 1} foo()
+modifies x, y;
+{
+ var b: bool;
+
+ call b := bar();
+ if (b) {
+ x := x + 1;
+ } else {
+ x := x - 1;
+ }
+}
+
+
+procedure main() returns (b: bool)
+requires x == y;
+ensures !b ==> x == y+1;
+ensures b ==> x+1 == y;
+modifies x, y;
+modifies y;
+{
+ call foo();
+ assert x == y;
+ call b := bar();
+}
diff --git a/Test/z3api/bar6.bpl b/Test/z3api/bar6.bpl new file mode 100644 index 00000000..e133aef7 --- /dev/null +++ b/Test/z3api/bar6.bpl @@ -0,0 +1,36 @@ +var M: [int]int;
+
+procedure {:inline 1} bar(y: int) returns (b: bool)
+modifies M;
+{
+ if (b) {
+ M[y] := M[y] + 1;
+ } else {
+ M[y] := M[y] - 1;
+ }
+}
+
+procedure {:inline 1} foo(x: int, y: int)
+modifies M;
+{
+ var b: bool;
+
+ call b := bar(y);
+ if (b) {
+ M[x] := M[x] + 1;
+ } else {
+ M[x] := M[x] - 1;
+ }
+}
+
+procedure main(x: int, y: int) returns (b: bool)
+requires x != y;
+requires M[x] == M[y];
+ensures !b ==> M[x] == M[y]+1;
+ensures b ==> M[x]+1 == M[y];
+modifies M;
+{
+ call foo(x, y);
+ assert M[x] == M[y];
+ call b := bar(y);
+}
diff --git a/Test/z3api/boog35.bpl b/Test/z3api/boog35.bpl new file mode 100644 index 00000000..beae0c74 --- /dev/null +++ b/Test/z3api/boog35.bpl @@ -0,0 +1,17 @@ +procedure foo1(x: int, y: int)
+{
+ var a: [int][int]int;
+
+ a[x][y] := 42;
+
+ assert a[x][y] == 42;
+}
+
+procedure foo2(x: int, y: int)
+{
+ var a: [int][int]int;
+
+ a[x][y] := 42;
+
+ assert a[x][y] == 43;
+}
\ No newline at end of file diff --git a/Test/z3api/runtest.bat b/Test/z3api/runtest.bat index e9bc968e..6645667e 100644 --- a/Test/z3api/runtest.bat +++ b/Test/z3api/runtest.bat @@ -3,15 +3,14 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog13.bpl boog14.bpl boog16.bpl boog17.bpl boog18.bpl boog20.bpl boog21.bpl boog22.bpl boog24.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do (
+for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog12.bpl boog13.bpl boog14.bpl boog15.bpl boog16.bpl boog17.bpl boog18.bpl boog19.bpl boog20.bpl boog21.bpl boog22.bpl boog23.bpl boog24.bpl boog25.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl boog35.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /typeEncoding:m /prover:z3api %%f
)
-REM boog12.bpl
-REM boog15.bpl
-
-REM boog19.bpl
-REM boog23.bpl
-REM boog25.bpl
\ No newline at end of file +for %%f in (bar1.bpl bar2.bpl bar3.bpl bar4.bpl bar6.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /stratifiedInline:1 /prover:z3api %%f
+)
\ No newline at end of file |