diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-08 18:47:21 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-08 18:47:21 +0000 |
| commit | 55aa6ae68bc1e4d8f8dc2a7a11fae477cdd95a32 (patch) | |
| tree | d2b4df86fbc9f31292b7aa06e162e4c0e6ffb787 | |
| parent | 2b7a6d2f2bcb26c0b5641bf7d0258c9fc9796c17 (diff) | |
Fixing the test case, it had a unary or. The cnf converter should be adapted to handle cases like this.
| -rw-r--r-- | test/regress/regress3/comb2.shuffled-as.sat03-420.smt | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress3/comb2.shuffled-as.sat03-420.smt b/test/regress/regress3/comb2.shuffled-as.sat03-420.smt index 19d6e6e24..b1d9309a3 100644 --- a/test/regress/regress3/comb2.shuffled-as.sat03-420.smt +++ b/test/regress/regress3/comb2.shuffled-as.sat03-420.smt @@ -141963,7 +141963,7 @@ :assumption (or x29226 x31829) :assumption (or x23991 (not x24837)) :assumption (or (not x14986) x23755) -:assumption (or (not x30806)) +:assumption (not x30806) :assumption (or (not x14192) (not x20229)) :assumption (or x4259 (not x10154)) :assumption (or (not x20740) (not x1847)) |