From e2adcc19ecc0f772db5adf05986b66a003cca255 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Jul 2015 22:52:44 -0700
Subject: [PATCH] fix unit test for default exception

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/test/ex.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/ex.cpp b/src/test/ex.cpp
index 276d21cab..e9243dd5b 100644
--- a/src/test/ex.cpp
+++ b/src/test/ex.cpp
@@ -54,7 +54,7 @@ static void tst1() {
 
 static void tst2() {
     try {
-        throw default_exception("Format %d %s", 12, "twelve");
+        throw default_exception(default_exception::fmt(), "Format %d %s", 12, "twelve");
     }
     catch (z3_exception& ex) {
         std::cerr << ex.msg() << "\n";