mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
parent
b93171de78
commit
5f22e98396
|
@ -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);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue