From ea8e9af7e428930898ba42d9a80ad725dee43cc7 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Andres=20N=C3=B6tzli?= Date: Thu, 22 Jun 2017 23:56:45 -0700 Subject: [PATCH] Fix assertion failure due to missing clause id (#180) This commit fixes bug 821. As written in the description of the bug, the issue is that `id` is not being set on one of the paths in addClause(), specifically in the case where all but one literal are assigned false and the remaining literal is assigned true. In that case, we are not actually adding anything and set the `id` to `ClauseIdUndef`. --- src/prop/minisat/core/Solver.cc | 5 ++++- test/regress/regress0/push-pop/Makefile.am | 3 ++- test/regress/regress0/push-pop/bug821.smt2 | 8 ++++++++ 3 files changed, 14 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/push-pop/bug821.smt2 diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 26af5f146..0bf5d5d7c 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -428,7 +428,10 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) } } return ok; - } else return ok; + } else { + PROOF(id = ClauseIdUndef;); + return ok; + } } } diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 197f81d63..0f2508144 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -49,7 +49,8 @@ BUG_TESTS = \ bug765.smt2 \ bug691.smt2 \ bug694-Unapply1.scala-0.smt2 \ - simple_unsat_cores.smt2 + simple_unsat_cores.smt2 \ + bug821.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/push-pop/bug821.smt2 b/test/regress/regress0/push-pop/bug821.smt2 new file mode 100644 index 000000000..b5371972a --- /dev/null +++ b/test/regress/regress0/push-pop/bug821.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +(set-logic UF) +(push 1) +(declare-fun _substvar_4_ () Bool) +(assert _substvar_4_) +(assert _substvar_4_) +(check-sat) -- 2.30.2