From 7fef5ff10436a51a91f57157f687345795f60e40 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 21 Jul 2016 14:37:28 +0200 Subject: [PATCH] Using $initstate in "initial assume" and "initial assert" --- frontends/ast/simplify.cc | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 4c64626f7..9f88cddc2 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -1387,7 +1387,12 @@ skip_dynamic_range_lvalue_expansion:; assign_check = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), new AstNode(AST_REDUCE_BOOL, children[0]->clone())); assign_check->children[0]->str = id_check; - assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(1, false, 1)); + if (current_always == nullptr || current_always->type != AST_INITIAL) { + assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(1, false, 1)); + } else { + assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), new AstNode(AST_FCALL)); + assign_en->children[1]->str = "\\$initstate"; + } assign_en->children[0]->str = id_en; newNode = new AstNode(AST_BLOCK); -- 2.30.2