Using $initstate in "initial assume" and "initial assert"

diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 4c64626f7924653faa274d26310a2b43ca71f576..9f88cddc2349ff414b968d579c39784f0c7b7a94 100644 (file)
--- 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);