Replaced INVARIANT(false) with UNREACHABLE_BECAUSE

Enrico Steffinlongo · Enrico Steffinlongo · commit 1a0f60d56f11 · 2023-04-18T10:37:56.000+01:00
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -516,10 +516,9 @@ constant_exprt smt2_convt::parse_literal(
     return from_integer(value, type);
   }
   else
-    INVARIANT(
-      false,
+    UNREACHABLE_BECAUSE(
       "smt2_convt::parse_literal should not be of unsupported type " +
-        type.id_string());
+      type.id_string());
 }
 
 exprt smt2_convt::parse_array(
diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp
@@ -232,7 +232,8 @@ add_axioms_for_format_specifier(
   }
   }
 
-  INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
+  UNREACHABLE_BECAUSE(
+    "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
 }
 
 /// Deserialize an argument for format from \p string.

Original file line number	Diff line number	Diff line change
`@@ -516,10 +516,9 @@ constant_exprt smt2_convt::parse_literal(`
`516`	`516`	`return from_integer(value, type);`
`517`	`517`	`}`
`518`	`518`	`else`
`519`		`- INVARIANT(`
`520`		`- false,`
	`519`	`+ UNREACHABLE_BECAUSE(`
`521`	`520`	`"smt2_convt::parse_literal should not be of unsupported type " +`
`522`		`- type.id_string());`
	`521`	`+ type.id_string());`
`523`	`522`	`}`
`524`	`523`
`525`	`524`	`exprt smt2_convt::parse_array(`
Original file line number	Diff line number	Diff line change
`@@ -232,7 +232,8 @@ add_axioms_for_format_specifier(`
`232`	`232`	`}`
`233`	`233`	`}`
`234`	`234`
`235`		`- INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");`
	`235`	`+ UNREACHABLE_BECAUSE(`
	`236`	`+ "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");`
`236`	`237`	`}`
`237`	`238`
`238`	`239`	`/// Deserialize an argument for format from \p string.`