From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 21 Jun 2013 15:15:57 +0000 (-0400)
Subject: Fix failure in non-assertion builds on incorrect SmtEngine use.
X-Git-Tag: cvc5-1.0.0~7287^2~33^2~2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e9f5d4eb49f62394d5696875e5fc1deed417a865;p=cvc5.git

Fix failure in non-assertion builds on incorrect SmtEngine use.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 76d4c973f..411d4ee3f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -791,6 +791,9 @@ SmtEngine::~SmtEngine() throw() {
 
 void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
   SmtScope smts(this);
+  if(d_fullyInited) {
+    throw ModalException("Cannot set logic in SmtEngine after the engine has finished initializing");
+  }
   d_logic = logic;
   setLogicInternal();
 }