diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-09 23:07:33 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-09 23:07:33 +0000 |
| commit | 044329296028ad944b703929fad4d85aa6183472 (patch) | |
| tree | b2a6d56fc5eb4d1bbc4d8d75a1b2814f5b4382be /test/regress/regress0/wiki.16.cvc | |
| parent | 0feb78d917ce5847ede01a5895611e54195bafcd (diff) | |
Changes to the CNF conversion and the SAT solver. All regression pass now, and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.
Diffstat (limited to 'test/regress/regress0/wiki.16.cvc')
| -rw-r--r-- | test/regress/regress0/wiki.16.cvc | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc new file mode 100644 index 000000000..af47433f8 --- /dev/null +++ b/test/regress/regress0/wiki.16.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND FALSE <=> FALSE; |