Incorporate datatypes into smt comp script, add regression.

diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017
index 6a0ef54b2a30a2c7889d8f1100e5ba4a2b491caa..ffa54bec925081a33400a89ab440fa2d9dc13d77 100644 (file)
--- a/contrib/run-script-smtcomp2017
+++ b/contrib/run-script-smtcomp2017
@@ -44,45 +44,44 @@ QF_NIA)
 QF_NRA)
   finishwith --nl-ext --nl-ext-tplanes
   ;;
-ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA)
+# all logics with UF + quantifiers should either fall under this or special cases below
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA)
   # the following is designed for a run time of 2400s (40 min).
   # initial runs 1min
   trywith 20 --simplification=none --full-saturate-quant
   trywith 20 --no-e-matching --full-saturate-quant
   trywith 20 --fs-inst --decision=internal --full-saturate-quant
-  # trigger selections 4min
+  # trigger selections 3min
   trywith 30 --relevant-triggers --full-saturate-quant
   trywith 30 --trigger-sel=max --full-saturate-quant
-  trywith 30 --trigger-sel=min-s-max --full-saturate-quant
   trywith 30 --multi-trigger-when-single --full-saturate-quant
   trywith 30 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
   trywith 30 --multi-trigger-cache --full-saturate-quant
   trywith 30 --no-multi-trigger-linear --full-saturate-quant
-  trywith 30 --literal-match=agg --full-saturate-quant
   # other 3min
   trywith 30 --pre-skolem-quant --full-saturate-quant
   trywith 30 --inst-when=full --full-saturate-quant
-  trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
   trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant
-  trywith 60 --nl-ext --full-saturate-quant
+  trywith 30 --nl-ext --full-saturate-quant
+  trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
   # finite model find 2min
-  trywith 30 --finite-model-find --mbqi=none
-  trywith 30 --finite-model-find
-  trywith 30 --finite-model-find --uf-ss=no-minimal
-  trywith 60 --finite-model-find --decision=internal
+  trywith 20 --finite-model-find --mbqi=none
+  trywith 20 --finite-model-find
+  trywith 20 --finite-model-find --uf-ss=no-minimal
+  trywith 60 --finite-model-find --fmf-inst-engine
   # long runs 20min
-  trywith 300 --decision=internal --full-saturate-quant
-  trywith 300 --term-db-mode=relevant --full-saturate-quant
-  trywith 300 --fs-inst --full-saturate-quant
-  trywith 300 --finite-model-find --fmf-inst-engine
+  trywith 200 --decision=internal --full-saturate-quant
+  trywith 200 --term-db-mode=relevant --full-saturate-quant
+  trywith 200 --fs-inst --full-saturate-quant
+  trywith 600 --finite-model-find --decision=internal
   # finite model find 1min
   trywith 30 --finite-model-find --fmf-bound-int
   trywith 30 --finite-model-find --sort-inference
-  # finish 9min
+  # finish 10min
   finishwith --full-saturate-quant
   ;;
 UFBV)
-  # many problems in UFBV are essentially BV
+  # most problems in UFBV are essentially BV
   trywith 300 --full-saturate-quant
   trywith 300 --full-saturate-quant --cbqi --decision=internal
   finishwith --finite-model-find

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index 048effcf1c7ba6a215d4404162ff16dda77f9046..98179df8c3d2de90a112146c5be37064cdb248a3 100644 (file)
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -51,7 +51,8 @@ TESTS =       \
        bug569.smt2 \
        div.09.smt2 \
        bug716.0.smt2 \
-       bug716.1.cvc
+       bug716.1.cvc \
+       mod-simp.smt2
 #      problem__003.smt2
 
 EXTRA_DIST = $(TESTS) \

diff --git a/test/regress/regress0/arith/mod-simp.smt2 b/test/regress/regress0/arith/mod-simp.smt2
new file mode 100644 (file)
index 0000000..1a9c505
--- /dev/null
+++ b/test/regress/regress0/arith/mod-simp.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_LIA)
+(set-info :status unsat)
+
+(declare-fun x () Int)
+
+(assert (not (= (mod (* 3 x) 10) (mod (* 3 (+ x 10)) 10))))
+
+(check-sat)