summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test/regress/regress0/Makefile.am2
-rw-r--r--test/regress/regress0/arith/Makefile.am1
-rw-r--r--test/regress/regress0/arith/integers/Makefile.am5
-rw-r--r--test/regress/regress0/auflia/Makefile.am1
-rw-r--r--test/regress/regress0/datatypes/Makefile.am1
-rw-r--r--test/regress/regress0/decision/Makefile.am9
-rw-r--r--test/regress/regress0/push-pop/Makefile.am3
-rw-r--r--test/regress/regress0/quantifiers/Makefile.am5
-rw-r--r--test/regress/regress0/uflia/Makefile.am4
-rw-r--r--test/regress/regress0/uflra/Makefile.am3
-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.am18
-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.smt29
-rw-r--r--test/regress/regress2/Makefile.am11
-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.expect3
-rwxr-xr-xtest/regress/run_regression9
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='' \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback