From 641c5eb5da6eebc417cc81af7caa714b766641c4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 9 Feb 2022 22:03:35 +0000 Subject: [PATCH] Make conversion failures in the propositional back-end fatal With the exception of some uses of quantifiers that should not be any cases left that are unsupported by the back-end (while generated by a sane front-end). --- src/solvers/prop/prop_conv_solver.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index b224ce95709..bb6c99730fd 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -424,9 +424,7 @@ void prop_conv_solvert::add_constraints_to_prop(const exprt &expr, bool value) void prop_conv_solvert::ignoring(const exprt &expr) { - // fall through - - log.warning() << "warning: ignoring " << expr.pretty() << messaget::eom; + INVARIANT(false, "No known conversion for " + expr.pretty()); } void prop_conv_solvert::finish_eager_conversion()