diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-09 13:49:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-09 15:49:10 -0500 |
| commit | c74e9c8ba946387616345b70d63028896a0022c2 (patch) | |
| tree | a7446c7a7682845073390801b4f4acc498baccce /test/regress/regress0/nl | |
| parent | 3740873b8b1ac7e1f2c203b26de6dd1a0ef73f43 (diff) | |
Make registration of unit clauses more robust (#3965)
Fixes #3959. It can happen that we generate a lemma that results in a
unit clause that matches a unit clause that was added as an input.
However, we are asserting that a unit clause can only be registered as
either one of them. This commit fixes the issue by only registering a
unit clause from a lemma if it is not already satisfied. I chose this
fix because the existing code doesn't seem to do anything (in terms of
solving) for the case where we have a unit clause that is already
satisfied because of an input unit clause.
Diffstat (limited to 'test/regress/regress0/nl')
| -rw-r--r-- | test/regress/regress0/nl/issue3959.smt2 | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress0/nl/issue3959.smt2 b/test/regress/regress0/nl/issue3959.smt2 new file mode 100644 index 000000000..cce64a848 --- /dev/null +++ b/test/regress/regress0/nl/issue3959.smt2 @@ -0,0 +1,12 @@ +; REQUIRES: proof +; COMMAND-LINE: --produce-unsat-cores --incremental +; EXPECT: sat + +; Note: the logic must include UF to trigger the bug +(set-logic QF_UFNIA) +(declare-const v10 Bool) +(declare-const i12 Int) +(declare-const i16 Int) +(push 1) +(assert (=> (<= (mod i12 38) i16) v10)) +(check-sat) |