From fe1290a6ebf13075628019040f68987cc55ce716 Mon Sep 17 00:00:00 2001
From: Jeannie Moulton <jeannie.moulton@diffblue.com>
Date: Thu, 6 Feb 2020 14:26:48 +0000
Subject: [PATCH] Catch and log invariant errors.

If cbmc_invariants_should_throwt is enabled, then invariants become
exceptions and we should log them instead of putting them into the catch
all with no information.
---
 src/util/parse_options.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp
index c1bece29bab..d9dbdac6e48 100644
--- a/src/util/parse_options.cpp
+++ b/src/util/parse_options.cpp
@@ -118,6 +118,11 @@ int parse_options_baset::main()
     log.error() << e.what() << messaget::eom;
     return CPROVER_EXIT_EXCEPTION;
   }
+  catch(const invariant_failedt &e)
+  {
+    log.error() << e.what() << messaget::eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
   catch(...)
   {
     log.error() << "Unknown exception type!" << messaget::eom;