From 62f99fbd2412105f57be71697acca297f2797b3a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 26 Dec 2024 19:32:54 +0000 Subject: [PATCH] SMV: typechecking for ?: This fixes type checking for SMV ?: --- src/smvlang/smv_typecheck.cpp | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index c1ed26f3a..953f03e44 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -836,9 +836,21 @@ void smv_typecheckt::typecheck_expr_rec( auto &false_case = if_expr.false_case(); typecheck_expr_rec(if_expr.cond(), mode); convert_expr_to(if_expr.cond(), bool_typet{}); - typecheck_expr_rec(true_case, dest_type, mode); - typecheck_expr_rec(false_case, dest_type, mode); - expr.type() = dest_type; + + if(dest_type.is_nil()) + { + typecheck_expr_rec(true_case, mode); + typecheck_expr_rec(false_case, mode); + expr.type() = type_union(true_case.type(), false_case.type()); + typecheck_expr_rec(true_case, expr.type(), mode); + typecheck_expr_rec(false_case, expr.type(), mode); + } + else + { + typecheck_expr_rec(true_case, dest_type, mode); + typecheck_expr_rec(false_case, dest_type, mode); + expr.type() = dest_type; + } } else if(expr.id()==ID_plus || expr.id()==ID_minus || expr.id()==ID_mult || expr.id()==ID_div ||