Merge pull request #984 from diffblue/smvlang-nondet-symbol

tautschnig · web-flow · commit 081b32253c50 · 2025-02-10T13:52:52.000+01:00
remove dead code in SMV typechecker
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
@@ -636,11 +636,6 @@ void smv_typecheckt::typecheck_expr_rec(
     expr.set(ID_C_smv_iff, true);
     expr.id(ID_equal);
   }
-  else if(expr.id()==ID_nondet_symbol)
-  {
-    if(!dest_type.is_nil())
-      expr.type() = dest_type;
-  }
   else if(expr.id()==ID_constraint_select_one)
   {
     typecheck_op(expr, dest_type, mode);

Original file line number	Diff line number	Diff line change
`@@ -636,11 +636,6 @@ void smv_typecheckt::typecheck_expr_rec(`
`636`	`636`	`expr.set(ID_C_smv_iff, true);`
`637`	`637`	`expr.id(ID_equal);`
`638`	`638`	`}`
`639`		`- else if(expr.id()==ID_nondet_symbol)`
`640`		`- {`
`641`		`- if(!dest_type.is_nil())`
`642`		`- expr.type() = dest_type;`
`643`		`- }`
`644`	`639`	`else if(expr.id()==ID_constraint_select_one)`
`645`	`640`	`{`
`646`	`641`	`typecheck_op(expr, dest_type, mode);`