From 9556a223f328718fdf28a250044dee5bf5c52787 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Mar 2014 00:54:14 -0700 Subject: [PATCH] check types Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 4 ++++ src/opt/opt_solver.cpp | 12 ++++++++---- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index de4156747..695b53395 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -82,6 +82,10 @@ namespace opt { unsigned context::add_objective(app* t, bool is_max) { app_ref tr(t, m); + arith_util a(m); + if (!a.is_arith_expr(t)) { + throw default_exception("Objective must be integer or real"); + } unsigned index = m_objectives.size(); m_objectives.push_back(objective(is_max, tr, index)); return index; diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 29cef424d..7b23161d6 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -261,10 +261,14 @@ namespace opt { } - void opt_solver::to_smt2_benchmark(std::ofstream & buffer, - unsigned num_assumptions, expr * const * assumptions, - char const * name, char const * logic, - char const * status, char const * attributes) { + void opt_solver::to_smt2_benchmark( + std::ofstream & buffer, + unsigned num_assumptions, + expr * const * assumptions, + char const * name, + char const * logic, + char const * status, + char const * attributes) { ast_smt_pp pp(m); pp.set_benchmark_name(name); pp.set_logic(logic);