SMV: typechecking for ?:

This fixes type checking for SMV ?:

Author: kroening

regression/smv/expressions/smv_if2.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 smv_if2.smv
-
+--bound 1
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This yields a type error.

regression/smv/expressions/smv_if2.smv

@@ -6,3 +6,5 @@ VAR b : 1..4;
 
 ASSIGN init(b) := 1;
 ASSIGN next(b) := (input ? 1 : 3) + 1;
+
+LTLSPEC X (b=2 | b=4)

src/smvlang/smv_typecheck.cpp

@@ -704,9 +704,21 @@ void smv_typecheckt::typecheck_expr_rec(
     auto &true_case = if_expr.true_case();
     auto &false_case = if_expr.false_case();
     typecheck_expr_rec(if_expr.cond(), bool_typet{}, mode);
-    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, nil_type, mode);
+      typecheck_expr_rec(false_case, nil_type, 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 ||