From 41ff29771593957ae546e6c68ef8e0d6ebe99f57 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 3 Jan 2025 10:19:41 +0000 Subject: [PATCH] fixup! IC3: better error message when given assumption --- regression/ebmc/ic3/not_supported3.desc | 2 +- src/ic3/m1ain.cc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/ebmc/ic3/not_supported3.desc b/regression/ebmc/ic3/not_supported3.desc index bf68c6f3..d31d3a54 100644 --- a/regression/ebmc/ic3/not_supported3.desc +++ b/regression/ebmc/ic3/not_supported3.desc @@ -2,6 +2,6 @@ CORE not_supported3.sv --ic3 ^no support for assumptions$ -^EXIT=1$ +^EXIT=10$ ^SIGNAL=0$ -- diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc index 36e63f03..c4cbf21c 100644 --- a/src/ic3/m1ain.cc +++ b/src/ic3/m1ain.cc @@ -111,7 +111,7 @@ property_checker_resultt ic3_enginet::operator()() if(property.is_assumed()) { message.error() << "no support for assumptions" << messaget::eom; - return 1; + return property_checker_resultt::error(); } }