diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 82f2dbc49..21a986fda 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -214,8 +214,11 @@ ATOMIC_CMD(labels_cmd, "labels", "retrieve Simplify-like labels", {
 ATOMIC_CMD(get_assertions_cmd, "get-assertions", "retrieve asserted terms when in interactive mode", ctx.display_assertions(););
 
 UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", CPK_SYMBOL, symbol const &, 
-          ctx.set_logic(arg); 
-          ctx.print_success(););
+          if (ctx.set_logic(arg))
+              ctx.print_success();
+          else
+              ctx.print_unsupported(symbol::null);
+          );
 
 UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, { 
     ctx.display(ctx.regular_stream(), arg);
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 8d48545e4..261af3092 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -621,14 +621,19 @@ bool cmd_context::supported_logic(symbol const & s) const {
         s == "QF_FPA" || s == "QF_FPABV";
 }
 
-void cmd_context::set_logic(symbol const & s) {
+bool cmd_context::set_logic(symbol const & s) {
     if (has_logic())
         throw cmd_exception("the logic has already been set");
     if (has_manager() && m_main_ctx) 
         throw cmd_exception("logic must be set before initialization");    
     if (!supported_logic(s)) {
-        warning_msg("unknown logic, ignoring set-logic command");
-        return; 
+        if (m_params.m_smtlib2_compliant) {
+            return false; 
+        }
+        else {
+            warning_msg("unknown logic, ignoring set-logic command");
+            return true;
+        }
     }
     m_logic = s;
     if (is_logic("QF_RDL") ||
@@ -640,6 +645,7 @@ void cmd_context::set_logic(symbol const & s) {
         is_logic("QF_UFNRA") ||
         is_logic("QF_UFLRA"))
         m_numeral_as_real = true;
+    return true;
 }
 
 std::string cmd_context::reason_unknown() const { 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 07b0cf456..22b2ea046 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -254,7 +254,7 @@ public:
     void reset_cancel() { set_cancel(false); }
     context_params  & params() { return m_params; }
     void global_params_updated(); // this method should be invoked when global (and module) params are updated.
-    void set_logic(symbol const & s);
+    bool set_logic(symbol const & s);
     bool has_logic() const { return m_logic != symbol::null; }
     symbol const & get_logic() const { return m_logic; }
     bool is_logic(char const * l_name) const { return has_logic() && strcmp(m_logic.bare_str(), l_name) == 0; }