From 04678d96282e7ef62346b5b0877201b3708115a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Aug 2013 17:56:07 -0700 Subject: [PATCH] improve error message when sorts are non-numeric Signed-off-by: Nikolaj Bjorner --- src/ast/dl_decl_plugin.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 4f0c9a75d..6d0823a24 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -657,7 +657,9 @@ namespace datalog { SASSERT(value == 1); return m.mk_true(); } - m.raise_exception("unrecognized sort"); + std::stringstream strm; + strm << "sort '" << mk_pp(s, m) << "' is not recognized as a sort that contains numeric values.\nUse Bool, BitVec, Int, Real, or a Finite domain sort"; + m.raise_exception(strm.str().c_str()); return 0; }