From c3edf8c8fad1276ee0821aaeae4b9b83bcd42db7 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 28 May 2018 18:28:38 -0700 Subject: [PATCH] Restore assertion in smt_clause --- src/smt/smt_clause.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_clause.cpp b/src/smt/smt_clause.cpp index 4266ab246..2b9b8dd3e 100644 --- a/src/smt/smt_clause.cpp +++ b/src/smt/smt_clause.cpp @@ -25,10 +25,10 @@ namespace smt { \brief Create a new clause. bool_var2expr_map is a mapping from bool_var -> expr, it is only used if save_atoms == true. */ - clause * clause::mk(ast_manager & m, unsigned num_lits, literal * lits, clause_kind k, justification * js, + clause * clause::mk(ast_manager & m, unsigned num_lits, literal * lits, clause_kind k, justification * js, clause_del_eh * del_eh, bool save_atoms, expr * const * bool_var2expr_map) { SASSERT(k == CLS_AUX || js == 0 || !js->in_region()); - SASSERT(num_lits > 2); + SASSERT(num_lits >= 2); unsigned sz = get_obj_size(num_lits, k, save_atoms, del_eh != nullptr, js != nullptr); void * mem = m.get_allocator().allocate(sz); clause * cls = new (mem) clause(); @@ -67,7 +67,7 @@ namespace smt { }}); return cls; } - + void clause::deallocate(ast_manager & m) { clause_del_eh * del_eh = get_del_eh(); if (del_eh) @@ -115,4 +115,3 @@ namespace smt { } }; -