diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp index 97de59283..5a26c0651 100644 --- a/src/ast/sls/sls_euf_plugin.cpp +++ b/src/ast/sls/sls_euf_plugin.cpp @@ -98,6 +98,8 @@ namespace sls { sat::literal l = to_literal(p); SASSERT(ctx.is_true(l)); lits.push_back(~l); + if (ctx.is_unit(l)) + continue; if (ctx.rand(++n) == 0) flit = l; }