mc: fix translation of local variable initializers

variable initializers were erroneously not executed if they were not a
proc call.

src/mc/mod.rs

@@ -206,7 +206,7 @@ fn translate_variables(
             let decl = var_ref.borrow();
             let mut comment = None;
             let initial_value = if let Some(initial_expr) = &decl.init {
-                if matches!(initial_expr.kind, ExprKind::Lit(_)) {
+                if is_constant(initial_expr) {
                     Some(Box::new(translate_expr(initial_expr)?))
                 } else {
                     let builder = ExprBuilder::new(Span::dummy_span());
@@ -418,3 +418,12 @@ fn extract_embed(expr: &Expr) -> Option<Expr> {
     }
     None
 }
+
+/// Whether an expression is a constant value and can be evaluated without any
+/// other variables.
+///
+/// Right now, we just check directly that it is a literal. In the future, one
+/// could allow more complex (constant) expressions as well.
+fn is_constant(expr: &Expr) -> bool {
+    matches!(expr.kind, ExprKind::Lit(_))
+}

src/mc/opsem.rs

@@ -16,7 +16,9 @@ use crate::{
     tyctx::TyCtx,
 };
 
-use super::{specs::SpecAutomaton, translate_expr, translate_ident, JaniConversionError};
+use super::{
+    is_constant, specs::SpecAutomaton, translate_expr, translate_ident, JaniConversionError,
+};
 
 /// Intermediate structure to build the JANI automaton for pGCL semantics with
 /// expected rewards.
@@ -86,7 +88,7 @@ fn translate_stmt(
         StmtKind::Var(decl_ref) => {
             let decl = decl_ref.borrow();
             match &decl.init {
-                Some(init) if !is_pure(init) => {
+                Some(init) if !is_constant(init) => {
                     translate_assign(automaton, span, translate_ident(decl.name), init, next)
                 }
                 Some(_) => Ok(next),
@@ -339,10 +341,6 @@ pub fn translate_block(
     translate_stmts(automaton, &block.node, next)
 }
 
-fn is_pure(expr: &Expr) -> bool {
-    !matches!(expr.kind, ExprKind::Call(_, _))
-}
-
 fn translate_assign(
     automaton: &mut OpAutomaton,
     span: Span,