From 8497bafa2e28d3d713543c636dc4a172473be125 Mon Sep 17 00:00:00 2001 From: Nicolas Berthier Date: Thu, 11 Apr 2013 16:52:17 +0200 Subject: [PATCH] Minor but correction in sigali output. - Translation to z3z now evaluates constant expressions instead of abstracting them. This non-feature could cause "false" synthesis failures due to non-translatable yet constant expressions possibly introduced by tomato (or manually), for instance `not false' in node `n' bellow: node n (a: bool) returns (ok: bool) contract assume true enforce ok with () let ok = a or not false; tel --- compiler/minils/sigali/sigalimain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index 5f93236..234d051 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -61,7 +61,7 @@ let current_inputs : IdentSet.t ref = ref IdentSet.empty let current_locals : IdentSet.t ref = ref IdentSet.empty let translate_static_exp se = - match se.se_desc with + match (Static.simplify QualEnv.empty se).se_desc with | Sint(v) -> Cint(v) | Sfloat(_) -> raise Untranslatable | Sbool(true)