Merge pull request #1143 from diffblue/invar1

SMV: disallow `next(...)` in `INVAR`

Author: tautschnig

regression/smv/invar/invar1.desc

@@ -0,0 +1,8 @@
+CORE
+invar1.smv
+--bound 20
+^\[.*\] G x != 10: PROVED up to bound 20$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/smv/invar/invar1.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR x : 1..10;
+
+ASSIGN init(x) := 1;
+ASSIGN next(x) := x = 10 ? 10 : x + 1;
+
+-- x won't reach 10, since we won't reach 3
+INVAR x != 3
+
+LTLSPEC G x != 10

regression/smv/invar/invar2.desc

@@ -0,0 +1,8 @@
+CORE
+invar2.smv
+
+^file .* line 6: next\(...\) is not allowed here$
+^EXIT=2$
+^SIGNAL=0$
+--
+--

regression/smv/invar/invar2.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR x : 1..10;
+
+-- next(...) is not allowed
+INVAR next(x) != 3

src/smvlang/smv_typecheck.cpp

@@ -49,6 +49,7 @@ class smv_typecheckt:public typecheckt
   typedef enum
   {
     INIT,
+    INVAR,
     TRANS,
     OTHER,
     LTL,
@@ -1562,6 +1563,10 @@ void smv_typecheckt::typecheck(
     return;
 
   case smv_parse_treet::modulet::itemt::INVAR:
+    typecheck(item.expr, INVAR);
+    convert_expr_to(item.expr, bool_typet{});
+    return;
+
   case smv_parse_treet::modulet::itemt::FAIRNESS:
     typecheck(item.expr, OTHER);
     convert_expr_to(item.expr, bool_typet{});