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()