From 7767a2362685e407a38b8efd5b534992a319a7c2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2014 21:37:37 -0700 Subject: [PATCH] improve error messages on incorrect parameter passing Signed-off-by: Nikolaj Bjorner --- src/cmd_context/context_params.cpp | 8 +++++++- src/smt/arith_eq_solver.cpp | 4 +++- src/util/gparams.cpp | 21 +++++++++++++++------ 3 files changed, 25 insertions(+), 8 deletions(-) diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index d796dc9b1..d1184fbc8 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -86,7 +86,13 @@ void context_params::set(char const * param, char const * value) { set_bool(m_smtlib2_compliant, param, value); } else { - throw default_exception("unknown parameter '%s'", p.c_str()); + param_descrs d; + collect_param_descrs(d); + std::stringstream strm; + strm << "unknown parameter '" << p << "'\n"; + strm << "Legal parameters are:\n"; + d.display(strm, 2, false, false); + throw default_exception(strm.str()); } } diff --git a/src/smt/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp index 41a61bf73..9a6868ff1 100644 --- a/src/smt/arith_eq_solver.cpp +++ b/src/smt/arith_eq_solver.cpp @@ -604,7 +604,9 @@ bool arith_eq_solver::solve_integer_equations_gcd( } SASSERT(g == r0[i]); } - SASSERT(abs(r0[i]).is_one()); + if (!abs(r0[i]).is_one()) { + return false; + } live.erase(live.begin()+live_pos); for (j = 0; j < live.size(); ++j) { row& r = rows[live[j]]; diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 1d9426390..04acf1ad9 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -201,7 +201,7 @@ public: } } - void throw_unknown_parameter(symbol const & param_name, symbol const & mod_name) { + void throw_unknown_parameter(symbol const & param_name, param_descrs const& d, symbol const & mod_name) { if (mod_name == symbol::null) { char const * new_name = get_new_param_name(param_name); if (new_name) { @@ -213,11 +213,20 @@ public: param_name.bare_str()); } else { - throw exception("unknown parameter '%s'", param_name.bare_str()); + std::stringstream strm; + strm << "unknown parameter '" << param_name << "'\n"; + strm << "Legal parameters are:\n"; + d.display(strm, 2, false, false); + throw default_exception(strm.str()); } } else { - throw exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str()); + std::stringstream strm; + strm << "unknown parameter '" << param_name << "' "; + strm << "at module '" << mod_name << "'\n"; + strm << "Legal parameters are:\n"; + d.display(strm, 2, false, false); + throw default_exception(strm.str()); } } @@ -225,7 +234,7 @@ public: param_kind k = d.get_kind(param_name); params_ref & ps = get_params(mod_name); if (k == CPK_INVALID) { - throw_unknown_parameter(param_name, mod_name); + throw_unknown_parameter(param_name, d, mod_name); } else if (k == CPK_UINT) { long val = strtol(value, 0, 10); @@ -312,7 +321,7 @@ public: std::string get_default(param_descrs const & d, symbol const & p, symbol const & m) { if (!d.contains(p)) { - throw_unknown_parameter(p, m); + throw_unknown_parameter(p, d, m); } char const * r = d.get_default(p); if (r == 0) @@ -478,7 +487,7 @@ public: throw exception("unknown module '%s'", m.bare_str()); } if (!d->contains(p)) - throw_unknown_parameter(p, m); + throw_unknown_parameter(p, *d, m); out << " name: " << p << "\n"; if (m != symbol::null) { out << " module: " << m << "\n";