diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-06-13 20:37:43 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-06-13 20:37:43 +0000 |
| commit | d0b33af0cf910ca7adb0357dad13e7e88baedebc (patch) | |
| tree | fc9c1fae8b7c4e9a26656e81314800852996e2f6 /test/regress/regress0/uflra/Makefile.am | |
| parent | 6acb8e96739df11859d3bca8a9e67bdaff5600c6 (diff) | |
- Added a loop to internally assert constraints that are marked as true.
- Changes how CongruenceManager reports conflicts.
- ConstraintDatabase can now detect and raise conflicts when doing unate propagation.
Diffstat (limited to 'test/regress/regress0/uflra/Makefile.am')
| -rw-r--r-- | test/regress/regress0/uflra/Makefile.am | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index ea707e549..189c96618 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -28,7 +28,8 @@ SMT_TESTS = \ pb_real_10_0200_10_26.smt \ pb_real_10_0200_10_29.smt \ incorrect2.smt \ - incorrect1.smt + incorrect1.smt \ + error1.smt # Regression tests for SMT2 inputs SMT2_TESTS = |