diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp
index 9c9b9ed62..49a8da09c 100644
--- a/src/cmd_context/extra_cmds/proof_cmds.cpp
+++ b/src/cmd_context/extra_cmds/proof_cmds.cpp
@@ -260,6 +260,8 @@ public:
     void add_literal(expr* e) override {
         if (m.is_proof(e))
             m_proof_hint = to_app(e);
+        else if (!m.is_bool(e))
+            throw default_exception("literal should be either a Proof or Bool");
         else
             m_lits.push_back(e);
     }