From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Mon, 8 Feb 2010 18:47:21 +0000 (+0000)
Subject: Fixing the test case, it had a unary or. The cnf converter should be adapted to handl... 
X-Git-Tag: cvc5-1.0.0~9270
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=55aa6ae68bc1e4d8f8dc2a7a11fae477cdd95a32;p=cvc5.git

Fixing the test case, it had a unary or. The cnf converter should be adapted to handle cases like this.
---

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))