Merge pull request #8518 from diffblue/smt2-exception

kroening · web-flow · commit fa299c55341e · 2024-12-17T10:49:06.000-08:00
SMT2: fix exception thrown when given unsupported expression
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -2493,7 +2493,8 @@ void smt2_convt::convert_expr(const exprt &expr)
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,
-      "smt2_convt::convert_expr should not be applied to unsupported type",
+      "smt2_convt::convert_expr should not be applied to unsupported "
+      "expression",
       expr.id_string());
 }
 

Original file line number	Diff line number	Diff line change
`@@ -2493,7 +2493,8 @@ void smt2_convt::convert_expr(const exprt &expr)`
`2493`	`2493`	`else`
`2494`	`2494`	`INVARIANT_WITH_DIAGNOSTICS(`
`2495`	`2495`	`false,`
`2496`		`- "smt2_convt::convert_expr should not be applied to unsupported type",`
	`2496`	`+ "smt2_convt::convert_expr should not be applied to unsupported "`
	`2497`	`+ "expression",`
`2497`	`2498`	`expr.id_string());`
`2498`	`2499`	`}`
`2499`	`2500`