From f1710e561884137332bbde132a7f9ec5a89eb588 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Jan 2014 16:06:47 -0800
Subject: [PATCH] check parameters

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index bc173963d..2e5a0f53f 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -53,6 +53,15 @@ namespace opt {
 
     unsigned context::add_soft_constraint(expr* f, rational const& w, symbol const& id) { 
         maxsmt* ms;
+        if (w.is_neg()) {
+            throw default_exception("Negative weight supplied. Weight should be positive");
+        }
+        if (w.is_zero()) {
+            throw default_exception("Zero weight supplied. Weight should be positive");
+        }
+        if (!m.is_bool(f)) {
+            throw default_exception("Soft constraint should be Boolean");
+        }
         if (!m_maxsmts.find(id, ms)) {
             ms = alloc(maxsmt, m);
             ms->updt_params(m_params);