From 5f22e983965f66c916fcae5301b62c045b1fa41f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 18 Jun 2023 10:05:34 -0700
Subject: [PATCH] fix #6766

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/extra_cmds/proof_cmds.cpp | 2 ++
 1 file changed, 2 insertions(+)

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);
     }