diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-06-12 21:11:15 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-06-12 21:11:15 +0000 |
| commit | 9348417ac5f12e8269a52a7c9b5a01a4aa558c74 (patch) | |
| tree | 0b983b0eed731d24bf102aecb2f5a9892984be8b /test/regress | |
| parent | bd346889a03d0b1c6ab56d18d39d966f4782a58c (diff) | |
Fix to SMT-LIBv1 parser: QF_UF declares sort "U", but other *UF* logics do not (e.g. QF_UFLIA).
Also fix a syntax error in a regression test (CVC4 is too lenient to catch it though---CVC3 tripped over it).
Also add additional parts for "make submission" in the top-level makefile
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/uflia/error0.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/uflia/error0.smt2 b/test/regress/regress0/uflia/error0.smt2 index 614645cb4..73177a252 100644 --- a/test/regress/regress0/uflia/error0.smt2 +++ b/test/regress/regress0/uflia/error0.smt2 @@ -3,7 +3,7 @@ (declare-sort U 0) (set-info :source "Currently this example asserts both a literal and its negation to a theory.") (set-info :status unsat) -(set-info :category industrial) +(set-info :category "industrial") (set-info :difficulty 0) (declare-fun arg0 () Int) (declare-fun arg1 () Int) |