diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-16 15:04:14 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-13 19:21:13 -0400 |
commit | 24b4ca565400d64b82626484044f72fd024477cd (patch) | |
tree | 0f35b74427607bf5f6d97ec3f0f109182be022fd | |
parent | 14776d0aeb833a7e728a27af6ef545f20b495f7f (diff) |
Move some regress benchmarks around that took too long, other test cleanup.
-rw-r--r-- | test/regress/regress0/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/arith/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/arith/integers/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/auflia/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/decision/Makefile.am | 9 | ||||
-rw-r--r-- | test/regress/regress0/push-pop/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/uflia/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/uflra/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress1/DTP_k2_n35_c175_s15.smt2 (renamed from test/regress/regress0/arith/DTP_k2_n35_c175_s15.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 (renamed from test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect (renamed from test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect) | 0 | ||||
-rw-r--r-- | test/regress/regress1/GEO123+1.minimized.smt2 (renamed from test/regress/regress0/GEO123+1.minimized.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/Makefile.am | 18 | ||||
-rw-r--r-- | test/regress/regress1/auflia-fuzz06.smt (renamed from test/regress/regress0/auflia/fuzz06.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/bug394.smt2 (renamed from test/regress/regress0/push-pop/bug394.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/error0.smt2 (renamed from test/regress/regress0/uflia/error0.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/error1.smt (renamed from test/regress/regress0/uflra/error1.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/piVC_5581bd.smt2 (renamed from test/regress/regress0/quantifiers/piVC_5581bd.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/typed_v1l50016-simp.cvc (renamed from test/regress/regress0/datatypes/typed_v1l50016-simp.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress1/uflia-error0.smt2 (renamed from test/regress/regress0/decision/uflia-error0.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/uflia-error0.smt2.expect (renamed from test/regress/regress0/decision/uflia-error0.smt2.expect) | 0 | ||||
-rw-r--r-- | test/regress/regress1/xs-09-16-3-4-1-5.decn.smt (renamed from test/regress/regress0/uflia/xs-09-16-3-4-1-5.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect (renamed from test/regress/regress0/decision/pp-regfile.smt.expect) | 0 | ||||
-rw-r--r-- | test/regress/regress1/xs-09-16-3-4-1-5.smt | 29 | ||||
-rw-r--r-- | test/regress/regress2/Makefile.am | 11 | ||||
-rw-r--r-- | test/regress/regress2/bug497.cvc (renamed from test/regress/regress0/bug497.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress2/incorrect1.smt (renamed from test/regress/regress0/uflra/incorrect1.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/incorrect2.smt (renamed from test/regress/regress0/uflra/incorrect2.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/pp-regfile.smt (renamed from test/regress/regress0/decision/pp-regfile.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/pp-regfile.smt.expect | 3 | ||||
-rwxr-xr-x | test/regress/run_regression | 9 |
33 files changed, 67 insertions, 37 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 80c377972..962c4180f 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -105,7 +105,6 @@ TPTP_TESTS = # Regression tests derived from bug reports BUG_TESTS = \ - GEO123+1.minimized.smt2 \ smt2output.smt2 \ bug32.cvc \ bug49.smt \ @@ -140,7 +139,6 @@ BUG_TESTS = \ bug480.smt2 \ bug484.smt2 \ bug486.cvc \ - bug497.cvc \ bug507.smt2 \ bug512.smt2 \ bug512.minimized.smt2 \ diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 6c5eded7c..246d36223 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -23,7 +23,6 @@ TESTS = \ delta-minimized-row-vector-bug.smt \ fuzz_3-eq.smt \ leq.01.smt \ - DTP_k2_n35_c175_s15.smt2 \ mod.01.smt2 \ mod.02.smt2 \ mod.03.smt2 \ diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am index c555ba413..eca78b58f 100644 --- a/test/regress/regress0/arith/integers/Makefile.am +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -31,8 +31,8 @@ TESTS = \ arith-int-048.cvc \ arith-int-050.cvc \ arith-int-084.cvc \ - arith-int-097.cvc \ - arith-int-085.cvc + arith-int-085.cvc \ + arith-int-097.cvc EXTRA_DIST = $(TESTS) \ arith-int-001.cvc \ @@ -121,7 +121,6 @@ EXTRA_DIST = $(TESTS) \ arith-int-099.cvc \ arith-int-100.cvc - FAILING_TESTS = \ arith-int-007.cvc \ arith-int-082.cvc \ diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index 5a6ab9e2b..85bda7bfe 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -20,7 +20,6 @@ TESTS = \ fuzz03.smt \ fuzz04.smt \ fuzz05.smt \ - fuzz06.smt \ fuzz-error232.smt \ fuzz-error1099.smt \ a17.smt \ diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index b95261d56..478d0d5f3 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -33,7 +33,6 @@ TESTS = \ empty_tuprec.cvc \ mutually-recursive.cvc \ rewriter.cvc \ - typed_v1l50016-simp.cvc \ typed_v10l30054.cvc \ typed_v1l80005.cvc \ typed_v2l30079.cvc \ diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index 42fedd480..969d20124 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -22,8 +22,6 @@ TESTS = \ quant-Arrays_Q1-noinfer.smt2 \ quant-ex1.smt2 \ quant-ex1.disable_miniscope.smt2 \ - uflia-error0.smt2 \ - uflia-xs-09-16-3-4-1-5.smt \ uflia-xs-09-16-3-4-1-5.delta03.smt \ aufbv-fuzz01.smt \ bug347.smt \ @@ -38,20 +36,13 @@ TESTS = \ pp-regfile.delta01.smt \ pp-regfile.delta02.smt -# Correct, but takes too long: -# pp-regfile.smt \ -# - EXTRA_DIST = $(TESTS) \ aufbv-fuzz01.smt.expect \ pp-regfile.delta01.smt.expect \ - uflia-error0.smt2.expect \ bitvec0.delta01.smt.expect \ pp-regfile.delta02.smt.expect \ uflia-xs-09-16-3-4-1-5.delta03.smt.expect \ bitvec0.smt.expect \ - pp-regfile.smt.expect \ - uflia-xs-09-16-3-4-1-5.smt.expect \ bitvec5.smt.expect \ quant-Arrays_Q1-noinfer.smt2.expect \ wchains010ue.delta02.smt.expect \ diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 0032c5645..16b0bbf85 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -38,8 +38,7 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) \ bug216.smt2.expect \ - bug396.smt2 \ - bug394.smt2 + bug396.smt2 # synonyms for "check" in this directory .PHONY: regress regress0 test diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 3e04c8437..31a27cb57 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -35,9 +35,8 @@ TESTS = \ smtlib384a03.smt2 \ smtlib46f14a.smt2 \ smtlibf957ea.smt2 \ - gauss_init_0030.fof.smt2 \ - piVC_5581bd.smt2 - + gauss_init_0030.fof.smt2 + # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index f5ded6b88..34fd797b6 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -17,12 +17,10 @@ MAKEFLAGS = -k # Regression tests for SMT inputs SMT_TESTS = \ - xs-09-16-3-4-1-5.smt \ xs-09-16-3-4-1-5.delta01.smt \ xs-09-16-3-4-1-5.delta02.smt \ xs-09-16-3-4-1-5.delta03.smt \ xs-09-16-3-4-1-5.delta04.smt \ - error0.smt2 \ error1.smt \ error0.delta01.smt \ simple_cyclic2.smt2 \ @@ -36,7 +34,6 @@ SMT2_TESTS = \ check04.smt2 \ DRAGON_11_e1_2450.ec.minimized.smt2 \ FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 \ - FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 \ FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 \ stalmark_e7_27_e7_31.ec.minimized.smt2 \ stalmark_e7_27_e7_31.ec.smt2 \ @@ -63,7 +60,6 @@ EXTRA_DIST = $(TESTS) \ check04.smt2.expect \ DRAGON_11_e1_2450.ec.minimized.smt2.expect \ FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect \ - FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \ speed2_e8_449_e8_517.ec.smt2.expect \ stalmark_e7_27_e7_31.ec.minimized.smt2.expect \ stalmark_e7_27_e7_31.ec.smt2.expect \ diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 3491909e3..ceade2038 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -32,11 +32,8 @@ SMT_TESTS = \ pb_real_10_0200_10_22.smt \ pb_real_10_0200_10_26.smt \ pb_real_10_0200_10_29.smt \ - incorrect2.smt \ - incorrect1.smt \ incorrect1.delta01.smt \ incorrect1.delta02.smt \ - error1.smt \ neq-deltacomp.smt \ fuzz01.smt diff --git a/test/regress/regress0/arith/DTP_k2_n35_c175_s15.smt2 b/test/regress/regress1/DTP_k2_n35_c175_s15.smt2 index 20f4bf5a9..20f4bf5a9 100644 --- a/test/regress/regress0/arith/DTP_k2_n35_c175_s15.smt2 +++ b/test/regress/regress1/DTP_k2_n35_c175_s15.smt2 diff --git a/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 b/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 index 25f006d30..25f006d30 100644 --- a/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 +++ b/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 diff --git a/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect b/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect index a06e9864e..a06e9864e 100644 --- a/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect +++ b/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect diff --git a/test/regress/regress0/GEO123+1.minimized.smt2 b/test/regress/regress1/GEO123+1.minimized.smt2 index 8cc1fa7fd..8cc1fa7fd 100644 --- a/test/regress/regress0/GEO123+1.minimized.smt2 +++ b/test/regress/regress1/GEO123+1.minimized.smt2 diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index bcbb0a618..a636a4f0f 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -18,6 +18,10 @@ MAKEFLAGS = -k # put it below in "TESTS +=" TESTS = bug136.smt \ bug148.smt \ + bug394.smt2 \ + DTP_k2_n35_c175_s15.smt2 \ + GEO123+1.minimized.smt2 \ + error1.smt \ friedman_n4_i5.smt \ hole7.cvc \ hole8.cvc \ @@ -28,9 +32,19 @@ TESTS = bug136.smt \ ooo.tag10.smt2 \ hash_sat_06_19.smt2 \ hash_sat_09_09.smt2 \ - ooo.rf6.smt2 + ooo.rf6.smt2 \ + auflia-fuzz06.smt \ + piVC_5581bd.smt2 \ + typed_v1l50016-simp.cvc \ + FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 \ + xs-09-16-3-4-1-5.smt \ + xs-09-16-3-4-1-5.decn.smt \ + uflia-error0.smt2 -EXTRA_DIST = $(TESTS) +EXTRA_DIST = $(TESTS) \ + FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \ + uflia-error0.smt2.expect \ + xs-09-16-3-4-1-5.decn.smt.expect #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/auflia/fuzz06.smt b/test/regress/regress1/auflia-fuzz06.smt index 88c2a9d5c..88c2a9d5c 100644 --- a/test/regress/regress0/auflia/fuzz06.smt +++ b/test/regress/regress1/auflia-fuzz06.smt diff --git a/test/regress/regress0/push-pop/bug394.smt2 b/test/regress/regress1/bug394.smt2 index cb2bc32a8..cb2bc32a8 100644 --- a/test/regress/regress0/push-pop/bug394.smt2 +++ b/test/regress/regress1/bug394.smt2 diff --git a/test/regress/regress0/uflia/error0.smt2 b/test/regress/regress1/error0.smt2 index 73177a252..73177a252 100644 --- a/test/regress/regress0/uflia/error0.smt2 +++ b/test/regress/regress1/error0.smt2 diff --git a/test/regress/regress0/uflra/error1.smt b/test/regress/regress1/error1.smt index 9b2cabedf..9b2cabedf 100644 --- a/test/regress/regress0/uflra/error1.smt +++ b/test/regress/regress1/error1.smt diff --git a/test/regress/regress0/quantifiers/piVC_5581bd.smt2 b/test/regress/regress1/piVC_5581bd.smt2 index 78baeea84..78baeea84 100644 --- a/test/regress/regress0/quantifiers/piVC_5581bd.smt2 +++ b/test/regress/regress1/piVC_5581bd.smt2 diff --git a/test/regress/regress0/datatypes/typed_v1l50016-simp.cvc b/test/regress/regress1/typed_v1l50016-simp.cvc index b273d99e9..b273d99e9 100644 --- a/test/regress/regress0/datatypes/typed_v1l50016-simp.cvc +++ b/test/regress/regress1/typed_v1l50016-simp.cvc diff --git a/test/regress/regress0/decision/uflia-error0.smt2 b/test/regress/regress1/uflia-error0.smt2 index 73177a252..73177a252 100644 --- a/test/regress/regress0/decision/uflia-error0.smt2 +++ b/test/regress/regress1/uflia-error0.smt2 diff --git a/test/regress/regress0/decision/uflia-error0.smt2.expect b/test/regress/regress1/uflia-error0.smt2.expect index b862d0b39..b862d0b39 100644 --- a/test/regress/regress0/decision/uflia-error0.smt2.expect +++ b/test/regress/regress1/uflia-error0.smt2.expect diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.smt b/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt index 549306c5b..549306c5b 100644 --- a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.smt +++ b/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt diff --git a/test/regress/regress0/decision/pp-regfile.smt.expect b/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect index b862d0b39..b862d0b39 100644 --- a/test/regress/regress0/decision/pp-regfile.smt.expect +++ b/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect diff --git a/test/regress/regress1/xs-09-16-3-4-1-5.smt b/test/regress/regress1/xs-09-16-3-4-1-5.smt new file mode 100644 index 000000000..549306c5b --- /dev/null +++ b/test/regress/regress1/xs-09-16-3-4-1-5.smt @@ -0,0 +1,29 @@ +(benchmark mathsat +:source { MathSat group } +:logic QF_UFLIA +:status unsat +:category { industrial } +:difficulty { 2 } +:extrafuns ((fmt1 Int)) +:extrafuns ((fmt0 Int)) +:extrafuns ((arg1 Int)) +:extrafuns ((arg0 Int)) +:extrafuns ((fmt_length Int)) +:extrafuns ((distance Int)) +:extrafuns ((adr_hi Int)) +:extrafuns ((adr_medhi Int)) +:extrafuns ((adr_medlo Int)) +:extrafuns ((adr_lo Int)) +:extrafuns ((select_format Int Int)) +:extrafuns ((percent Int)) +:extrafuns ((s Int)) +:extrafuns ((s_count Int Int)) +:extrafuns ((x Int)) +:extrafuns ((x_count Int Int)) +:formula +(flet ($concval (and (and (and (and (and (and (and (and (= distance 16) (= fmt_length 9)) (= adr_lo 3)) (= adr_medlo 4)) (= adr_medhi 1)) (= adr_hi 5)) (= percent 37)) (= s 115)) (= x 120))) +(flet ($attack (and (and (and (and (and (and (and (= fmt0 0) (= arg0 (- fmt0 distance))) (>= arg1 fmt0)) (< fmt1 (- (+ fmt0 fmt_length) 1))) (> fmt1 (+ fmt0 1))) (>= arg1 (+ arg0 distance))) (< arg1 (- (+ (+ arg0 distance) fmt_length) 4))) (= arg1 (+ (+ arg0 (* 4 (s_count (- (- fmt1 2) fmt0)))) (* 4 (x_count (- (- fmt1 2) fmt0))))))) +(flet ($restrict (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (= (select_format 0) percent) (= (select_format 0) s)) (= (select_format 0) x)) (= (select_format 0) adr_lo)) (= (select_format 0) adr_medlo)) (= (select_format 0) adr_medhi)) (= (select_format 0) adr_hi)) (= (select_format 0) 255)) (= (select_format 1) percent)) (= (select_format 1) s)) (= (select_format 1) x)) (= (select_format 1) adr_lo)) (= (select_format 1) adr_medlo)) (= (select_format 1) adr_medhi)) (= (select_format 1) adr_hi)) (= (select_format 1) 255)) (= (select_format 2) percent)) (= (select_format 2) s)) (= (select_format 2) x)) (= (select_format 2) adr_lo)) (= (select_format 2) adr_medlo)) (= (select_format 2) adr_medhi)) (= (select_format 2) adr_hi)) (= (select_format 2) 255)) (= (select_format 3) percent)) (= (select_format 3) s)) (= (select_format 3) x)) (= (select_format 3) adr_lo)) (= (select_format 3) adr_medlo)) (= (select_format 3) adr_medhi)) (= (select_format 3) adr_hi)) (= (select_format 3) 255)) (= (select_format 4) percent)) (= (select_format 4) s)) (= (select_format 4) x)) (= (select_format 4) adr_lo)) (= (select_format 4) adr_medlo)) (= (select_format 4) adr_medhi)) (= (select_format 4) adr_hi)) (= (select_format 4) 255)) (= (select_format 5) percent)) (= (select_format 5) s)) (= (select_format 5) x)) (= (select_format 5) adr_lo)) (= (select_format 5) adr_medlo)) (= (select_format 5) adr_medhi)) (= (select_format 5) adr_hi)) (= (select_format 5) 255)) (= (select_format 6) percent)) (= (select_format 6) s)) (= (select_format 6) x)) (= (select_format 6) adr_lo)) (= (select_format 6) adr_medlo)) (= (select_format 6) adr_medhi)) (= (select_format 6) adr_hi)) (= (select_format 6) 255)) (= (select_format 7) percent)) (= (select_format 7) s)) (= (select_format 7) x)) (= (select_format 7) adr_lo)) (= (select_format 7) adr_medlo)) (= (select_format 7) adr_medhi)) (= (select_format 7) adr_hi)) (= (select_format 7) 255)) (= (select_format 8) percent)) (= (select_format 8) s)) (= (select_format 8) x)) (= (select_format 8) adr_lo)) (= (select_format 8) adr_medlo)) (= (select_format 8) adr_medhi)) (= (select_format 8) adr_hi)) (= (select_format 8) 255))) +(flet ($counterdef (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (if_then_else (and (= (select_format 0) percent) (= (select_format 1) s)) (= (s_count 0) 1) (= (s_count 0) 0)) (if_then_else (and (= (select_format 1) percent) (= (select_format 2) s)) (= (s_count 1) (+ (s_count 0) 1)) (= (s_count 1) (s_count 0)))) (if_then_else (and (= (select_format 2) percent) (= (select_format 3) s)) (= (s_count 2) (+ (s_count 1) 1)) (= (s_count 2) (s_count 1)))) (if_then_else (and (= (select_format 3) percent) (= (select_format 4) s)) (= (s_count 3) (+ (s_count 2) 1)) (= (s_count 3) (s_count 2)))) (if_then_else (and (= (select_format 4) percent) (= (select_format 5) s)) (= (s_count 4) (+ (s_count 3) 1)) (= (s_count 4) (s_count 3)))) (if_then_else (and (= (select_format 5) percent) (= (select_format 6) s)) (= (s_count 5) (+ (s_count 4) 1)) (= (s_count 5) (s_count 4)))) (if_then_else (and (= (select_format 6) percent) (= (select_format 7) s)) (= (s_count 6) (+ (s_count 5) 1)) (= (s_count 6) (s_count 5)))) (if_then_else (and (= (select_format 7) percent) (= (select_format 8) s)) (= (s_count 7) (+ (s_count 6) 1)) (= (s_count 7) (s_count 6)))) (if_then_else (and (= (select_format 8) percent) (= (select_format 9) s)) (= (s_count 8) (+ (s_count 7) 1)) (= (s_count 8) (s_count 7)))) (if_then_else (and (= (select_format 0) percent) (= (select_format 1) x)) (= (x_count 0) 1) (= (x_count 0) 0))) (if_then_else (and (= (select_format 1) percent) (= (select_format 2) x)) (= (x_count 1) (+ (x_count 0) 1)) (= (x_count 1) (x_count 0)))) (if_then_else (and (= (select_format 2) percent) (= (select_format 3) x)) (= (x_count 2) (+ (x_count 1) 1)) (= (x_count 2) (x_count 1)))) (if_then_else (and (= (select_format 3) percent) (= (select_format 4) x)) (= (x_count 3) (+ (x_count 2) 1)) (= (x_count 3) (x_count 2)))) (if_then_else (and (= (select_format 4) percent) (= (select_format 5) x)) (= (x_count 4) (+ (x_count 3) 1)) (= (x_count 4) (x_count 3)))) (if_then_else (and (= (select_format 5) percent) (= (select_format 6) x)) (= (x_count 5) (+ (x_count 4) 1)) (= (x_count 5) (x_count 4)))) (if_then_else (and (= (select_format 6) percent) (= (select_format 7) x)) (= (x_count 6) (+ (x_count 5) 1)) (= (x_count 6) (x_count 5)))) (if_then_else (and (= (select_format 7) percent) (= (select_format 8) x)) (= (x_count 7) (+ (x_count 6) 1)) (= (x_count 7) (x_count 6)))) (if_then_else (and (= (select_format 8) percent) (= (select_format 9) x)) (= (x_count 8) (+ (x_count 7) 1)) (= (x_count 8) (x_count 7))))) +(flet ($integral (and (or (or (or (or (or (or (or (or (= fmt1 (+ fmt0 0)) (= fmt1 (+ fmt0 1))) (= fmt1 (+ fmt0 2))) (= fmt1 (+ fmt0 3))) (= fmt1 (+ fmt0 4))) (= fmt1 (+ fmt0 5))) (= fmt1 (+ fmt0 6))) (= fmt1 (+ fmt0 7))) (= fmt1 (+ fmt0 8))) (or (or (or (or (or (= arg1 (+ fmt0 0)) (= arg1 (+ fmt0 1))) (= arg1 (+ fmt0 2))) (= arg1 (+ fmt0 3))) (= arg1 (+ fmt0 4))) (= arg1 (+ fmt0 5))))) +(and (and (and (and (and $concval $attack) $restrict) $counterdef) $integral) (not (and (and (and (and (and (= (select_format fmt1) percent) (= (select_format (+ fmt1 1)) s)) (= (select_format arg1) adr_lo)) (= (select_format (+ arg1 1)) adr_medlo)) (= (select_format (+ arg1 2)) adr_medhi)) (= (select_format (+ arg1 3)) adr_hi)))))))))) diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index e0524b694..028eb4cc8 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -23,9 +23,14 @@ TESTS = bmc-ibm-1.smt \ friedman_n6_i4.smt \ hole9.cvc \ qwh.35.405.shuffled-as.sat03-1651.smt \ - eq_diamond14.smt - -EXTRA_DIST = $(TESTS) + eq_diamond14.smt \ + incorrect1.smt \ + incorrect2.smt \ + bug497.cvc \ + pp-regfile.smt + +EXTRA_DIST = $(TESTS) \ + pp-regfile.smt.expect #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/bug497.cvc b/test/regress/regress2/bug497.cvc index ce34ab6ad..ce34ab6ad 100644 --- a/test/regress/regress0/bug497.cvc +++ b/test/regress/regress2/bug497.cvc diff --git a/test/regress/regress0/uflra/incorrect1.smt b/test/regress/regress2/incorrect1.smt index 23425d462..23425d462 100644 --- a/test/regress/regress0/uflra/incorrect1.smt +++ b/test/regress/regress2/incorrect1.smt diff --git a/test/regress/regress0/uflra/incorrect2.smt b/test/regress/regress2/incorrect2.smt index 23425d462..23425d462 100644 --- a/test/regress/regress0/uflra/incorrect2.smt +++ b/test/regress/regress2/incorrect2.smt diff --git a/test/regress/regress0/decision/pp-regfile.smt b/test/regress/regress2/pp-regfile.smt index e60be055a..e60be055a 100644 --- a/test/regress/regress0/decision/pp-regfile.smt +++ b/test/regress/regress2/pp-regfile.smt diff --git a/test/regress/regress2/pp-regfile.smt.expect b/test/regress/regress2/pp-regfile.smt.expect new file mode 100644 index 000000000..b862d0b39 --- /dev/null +++ b/test/regress/regress2/pp-regfile.smt.expect @@ -0,0 +1,3 @@ +% COMMAND-LINE: --decision=justification +% EXPECT: unsat +% EXIT: 20 diff --git a/test/regress/run_regression b/test/regress/run_regression index a67496514..e9c17a3af 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -237,16 +237,18 @@ cvc4base=`basename "$cvc4"` cvc4full="$cvc4dirfull/$cvc4base" if [ $dump = no ]; then echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`] + time ( :; \ ( cd `dirname "$benchmark"`; $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"`; echo $? >"$exitstatusfile" - ) > "$outfile" 2> "$errfile" + ) > "$outfile" 2> "$errfile" ) else echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q --segv-nospin `basename "$benchmark"` \| $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --lang=smt2 - [from working dir `dirname "$benchmark"`] + time ( :; \ ( cd `dirname "$benchmark"`; $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q --segv-nospin `basename "$benchmark"` | $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --lang=smt2 -; echo $? >"$exitstatusfile" - ) > "$outfile" 2> "$errfile" + ) > "$outfile" 2> "$errfile" ) fi diffs=`diff -u --strip-trailing-cr "$expoutfile" "$outfile"` @@ -277,10 +279,11 @@ if [ "$proof" = yes -a "$expected_proof" = yes ]; then cp "$benchmark" "$pfbenchmark"; echo "$proof_command" >>"$pfbenchmark"; echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`] + time ( :; \ ( cd `dirname "$pfbenchmark"`; $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"`; echo $? >"$exitstatusfile" - ) > "$outfile" 2> "$errfile" + ) > "$outfile" 2> "$errfile" ) gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX diff --unchanged-group-format='' \ |