From 3bcb3a5f09ab9def080c117c64656152a8d500bb Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 26 Feb 2018 09:15:27 +0000
Subject: [PATCH] Fix decision procedure runtime computation

Follow-up for 2dc9fcd811.
---
 regression/cbmc/Failing_Assert1/test.desc | 1 +
 src/cbmc/bmc.cpp                          | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/regression/cbmc/Failing_Assert1/test.desc b/regression/cbmc/Failing_Assert1/test.desc
index 6de79559914..6137d7126bc 100644
--- a/regression/cbmc/Failing_Assert1/test.desc
+++ b/regression/cbmc/Failing_Assert1/test.desc
@@ -4,5 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+^Runtime decision procedure: [0-9]+(\.[0-9]+)?s$
 --
 ^warning: ignoring
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 1aa7efdf0fd..45d7829544f 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -170,7 +170,7 @@ bmct::run_decision_procedure(prop_convt &prop_conv)
   {
     auto solver_stop = std::chrono::steady_clock::now();
     status() << "Runtime decision procedure: "
-             << std::chrono::duration<double>(solver_start-solver_stop).count()
+             << std::chrono::duration<double>(solver_stop-solver_start).count()
              << "s" << eom;
   }