diff options
| author |  rustanleino <unknown> | 2009-10-04 07:01:06 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-10-04 07:01:06 +0000 |
| commit | f0df4f110687974508a4c96e4ebb58a9cd7270c8 (patch) | |
| tree | b4ec1a6714d898c8f58057306a90ff40747d6be9 /Source/VCExpr | |
| parent | bdaa9996170aed0b2638962014fe80777b98d5c7 (diff) | |
Added /z3lets switch, which governs which kinds of LET expressions are sent to Z3. By default, both LET TERM and LET FORMULA expressions are used. Mode /z3lets:2 uses only LET FORMULA, which works around a current Z3 issue with LET expressions and nested quantifiers.
Diffstat (limited to 'Source/VCExpr')
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.ssc | 9 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasure.ssc | 6 |
2 files changed, 6 insertions, 9 deletions
diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc index 7b6bb5c8..289dff87 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.ssc +++ b/Source/VCExpr/SimplifyLikeLineariser.ssc @@ -93,18 +93,15 @@ namespace Microsoft.Boogie.VCExprAST public class SimplifyLikeExprLineariser : IVCExprVisitor<bool, LineariserOptions!> {
public static string! ToSimplifyString(VCExpr! e, UniqueNamer! namer) {
- StringWriter sw = new StringWriter();
- SimplifyLikeExprLineariser! lin = new SimplifyLikeExprLineariser (sw, namer);
- lin.Linearise(e, LineariserOptions.SimplifyDefault);
- return (!)sw.ToString();
+ return ToString(e, LineariserOptions.SimplifyDefault, namer);
}
public static string! ToString(VCExpr! e, LineariserOptions! options,
UniqueNamer! namer) {
StringWriter sw = new StringWriter();
- SimplifyLikeExprLineariser! lin = new SimplifyLikeExprLineariser (sw, namer);
+ SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser (sw, namer);
lin.Linearise(e, options);
- return (!)sw.ToString();
+ return sw.ToString();
}
////////////////////////////////////////////////////////////////////////////////////////
diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc index 8347d124..f282b342 100644 --- a/Source/VCExpr/TypeErasure.ssc +++ b/Source/VCExpr/TypeErasure.ssc @@ -708,9 +708,9 @@ namespace Microsoft.Boogie.TypeErasure // "AbstractionVariable(int)" delivers variables
TypeSeq! instantiations) {
- if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))
- return rawType;
-
+ if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))
+ return rawType;
+
if (forall{TypeVariable! var in rawType.FreeVariables;
!boundTypeParams.Has(var)}) {
// Bingo!
|