From 58c511a607a7a3560590b49f17ee3e92b364dbcf Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 27 Aug 2012 19:27:28 +0000 Subject: * Reversing commit r4258 (which disabled failing regressions). Fixed the problem so they're no longer failing (in the quantifiers rewriter). Resolves bug #381. * Added LAMBDA kind and type rule, and Node::isClosure(). (this commit was certified error- and warning-free by the test-and-commit script.) --- test/regress/regress0/quantifiers/Makefile.am | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) (limited to 'test/regress') diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 8880bf3ca..38cc59125 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -28,16 +28,13 @@ TESTS = \ opisavailable-12.smt2 \ ricart-agrawala6.smt2 \ set8.smt2 \ + smtlib384a03.smt2 \ + smtlib46f14a.smt2 \ + smtlibf957ea.smt2 \ + gauss_init_0030.fof.smt2 \ + piVC_5581bd.smt2 \ set3.smt2 -# removed because failing -# smtlib384a03.smt2 \ -# smtlib46f14a.smt2 \ -# smtlibf957ea.smt2 \ -# gauss_init_0030.fof.smt2 \ -# piVC_5581bd.smt2 \ -# - # removed because it now reports unknown # symmetric_unsat_7.smt2 \ # -- cgit v1.2.3