$(REG2_TESTS) \
$(REG3_TESTS) \
$(REG4_TESTS) \
- $(TESTS_EXPECT) \
regress0/uf/mkpidgeon \
regress0/tptp/Axioms/BOO004-0.ax \
regress0/tptp/Axioms/SYN000+0.ax \
regress2/quantifiers/small-bug1-fixpoint-3.smt2 \
regress2/xs-11-20-5-2-5-3.smt \
regress2/xs-11-20-5-2-5-3.smt2
-
-TESTS_EXPECT = \
- regress0/arith/miplib-opt1217--27.smt.expect \
- regress0/arith/miplib-pp08a-3000.smt.expect \
- regress0/decision/aufbv-fuzz01.smt.expect \
- regress0/decision/bitvec0.delta01.smt.expect \
- regress0/decision/bitvec0.smt.expect \
- regress0/decision/bitvec5.smt.expect \
- regress0/decision/bug347.smt.expect \
- regress0/decision/bug374a.smt.expect \
- regress0/decision/bug374b.smt2.expect \
- regress0/decision/just_sat.expect \
- regress0/decision/just_unsat.expect \
- regress0/decision/pp-regfile.delta01.smt.expect \
- regress0/decision/pp-regfile.delta02.smt.expect \
- regress0/decision/quant-ex1.smt2.expect \
- regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt.expect \
- regress0/decision/uflia-xs-09-16-3-4-1-5.smt.expect \
- regress0/decision/wchains010ue.delta02.smt.expect \
- regress0/decision/wchains010ue.smt.expect \
- regress0/expect/scrub.01.smt.expect \
- regress0/expect/scrub.03.smt2.expect \
- regress0/quantifiers/bug291.smt2.expect \
- regress0/uflia/check02.smt2.expect \
- regress0/uflia/check03.smt2.expect \
- regress0/uflia/check04.smt2.expect \
- regress0/uflia/check04.smt2.expect \
- regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect \
- regress0/uflia/tiny.smt2.expect \
- regress1/bug216.smt2.expect \
- regress1/bug590.smt2.expect \
- regress1/decision/quant-Arrays_Q1-noinfer.smt2.expect \
- regress1/decision/quant-symmetric_unsat_7.smt2.expect \
- regress1/push-pop/bug216.smt2.expect \
- regress1/simplification_bug4.smt2.expect \
- regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect \
- regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect \
- regress1/uflia/speed2_e8_449_e8_517.ec.smt2.expect \
- regress1/uflia/stalmark_e7_27_e7_31.ec.smt2.expect \
- regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \
- regress2/uflia-error0.smt2.expect \
- regress2/xs-09-16-3-4-1-5.decn.smt.expect \
- regress3/pp-regfile.smt.expect
as a requirement, refer to CVC4's `--show-config` output. Features can also be
excluded by adding the `no-` prefix, e.g. `no-symfpu` means that the test is
not valid for builds that include symfpu support.
-
-Sometimes it is useful to keep the directives separate. You can separate the
-benchmark from the output expectations by putting the benchmark in `<benchmark
-file>.smt` and the directives in `<benchmark file>.smt.expect`, which is looked
-for by the regression script. Note that `*.expect` files should be added to the
-`EXTRA_DIST` variable in [Makefile.am](Makefile.am).
+; COMMAND-LINE: --miplib-trick
+; EXPECT: unsat
+
(benchmark mip_opt1217
:source {
Relaxation of the Mixed-Integer Programming
+++ /dev/null
-% COMMAND-LINE: --miplib-trick
-% EXPECT: unsat
+; COMMAND-LINE: --miplib-trick
+; EXPECT: unsat
+
(benchmark mip_pp08a
:source {
Relaxation of the Mixed-Integer Programming
+++ /dev/null
-% COMMAND-LINE: --miplib-trick
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification
+; EXPECT: sat
+
(benchmark fuzzsmt
:logic QF_AUFBV
:status sat
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: sat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(benchmark bitvec0.smt
:logic QF_BV
:extrafuns ((t BitVec[32]))
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(benchmark bitvec0.smt
:source {
Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite.
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(benchmark bitvec5.smt
:source {
Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite.
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification
+; EXPECT: sat
+
(benchmark B_
:status sat
:category { unknown }
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: sat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(benchmark fuzzsmt
:logic AUFLIA
:status unknown
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification --no-unconstrained
+; EXPECT: unsat
+
(set-logic QF_ALL_SUPPORTED)
(declare-fun _substvar_245_ () Bool)
(declare-fun _substvar_246_ () Bool)
+++ /dev/null
-% COMMAND-LINE: --decision=justification --no-unconstrained
-% EXPECT: unsat
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: sat
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(benchmark pp_regfile.smt
:logic QF_AUFLIA
:extrafuns ((REGFILE_INIT Array))
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(benchmark pp_regfile.smt
:logic QF_AUFLIA
:extrafuns ((REGFILE_INIT Array))
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification
+; EXPECT: sat
+
(set-logic AUFLIRA)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: sat
+; COMMAND-LINE: --decision=justification
+; EXPECT: sat
+
(benchmark mathsat
:logic QF_UFLIA
:extrafuns ((fmt_length Int))
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: sat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(benchmark mathsat
:source { MathSat group }
:logic QF_UFLIA
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(benchmark wchains010ue.smt
:logic QF_AUFBV
:extrafuns ((v6 BitVec[32]))
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(benchmark wchains010ue.smt
:source {
This benchmark generates write chain permutations and tries to show
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
+; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
+; EXPECT: The fact in question: TERM
+; EXPECT: ")
+; EXIT: 1
+
(benchmark reject_nonlinear
:logic QF_LRA
:extrafuns ((n Real))
+++ /dev/null
-% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
-% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
-% EXPECT: The fact in question: TERM
-% EXPECT: ")
-% EXIT: 1
+; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
+; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
+; EXPECT: The fact in question: TERM
+; EXPECT: ")
+; EXIT: 1
+
(set-logic QF_LRA)
(set-info :status unknown)
(declare-fun n () Real)
+++ /dev/null
-% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
-% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
-% EXPECT: The fact in question: TERM
-% EXPECT: ")
-% EXIT: 1
+; EXPECT: unknown
+; EXPECT: (:reason-unknown incomplete)
(set-logic AUFLIA)
(set-info :source |
Boogie/Spec# benchmarks.
+++ /dev/null
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)
\ No newline at end of file
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+
(set-logic QF_UFLIA)
(declare-fun b () Int)
(declare-fun n () Int)
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: sat
-% EXPECT: unsat
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+
(set-logic QF_UFLIA)
(declare-fun _n () Int)
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: sat
-% EXPECT: unsat
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+
(set-logic QF_LIA)
(declare-fun _b () Int)
(declare-fun _n () Int)
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: sat
-% EXPECT: unsat
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+
(set-logic QF_UFLIA)
(declare-fun _base () Int)
(declare-fun _n () Int)
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: sat
-% EXPECT: unsat
+; COMMAND-LINE: --incremental --simplification=none
+; EXPECT: sat
+; EXPECT: unsat
+
(set-logic QF_UFLIA)
(declare-fun base () Int)
(declare-fun n () Int)
+++ /dev/null
-% COMMAND-LINE: --incremental --simplification=none
-% EXPECT: sat
-% EXPECT: unsat
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+
(set-logic QF_UF)
(declare-fun x () Bool)
(declare-fun y () Bool)
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: sat
-% EXPECT: unsat
+; EXPECT: unknown
+; EXPECT: ((charlst2 ((as const (Array Int String)) "")))
+
(set-logic QF_ALL_SUPPORTED)
(set-option :strings-exp true)
(set-option :produce-models true)
+++ /dev/null
-% EXPECT: unknown
-% EXPECT: ((charlst2 ((as const (Array Int String)) "")))
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(set-logic AUFLIA)
(set-info :source |
Boogie/Spec# benchmarks.
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores --decision=justification
+; EXPECT: unsat
+
(set-logic AUFLIRA)
(set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods.
+++ /dev/null
-% COMMAND-LINE: --no-check-proofs --no-check-unsat-cores --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+
(set-logic QF_UF)
(declare-fun x () Bool)
(declare-fun y () Bool)
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: sat
-% EXPECT: unsat
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+
(set-logic QF_LIA)
;; Simplified benchmark, derived from NuSMV output durationThm_1.bmc_k100.smt2
;;
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: unsat
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+
(set-logic QF_UFLIA)
(declare-fun _base () Int)
(declare-fun _n () Int)
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: sat
-% EXPECT: sat
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+
(set-logic QF_UFLIA)
(set-info :smt-lib-version 2.0)
(declare-fun _base () Int)
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: sat
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+
(set-logic QF_UFLIA)
(declare-fun _base () Int)
(declare-fun _n () Int)
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: unsat
-% EXPECT: sat
-% EXPECT: unsat
-% EXPECT: unsat
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+
(set-logic QF_UFLIA)
(declare-fun _base () Int)
(declare-fun _n () Int)
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: unsat
-% EXPECT: sat
-% EXPECT: unsat
-% EXPECT: sat
-% EXPECT: unsat
-% EXPECT: unsat
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+
(set-logic QF_UFLIA)
(declare-fun _base () Int)
(declare-fun _n () Int)
+++ /dev/null
-% COMMAND-LINE: --incremental
-% EXPECT: unsat
-% EXPECT: sat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(set-logic QF_UFLIA)
(declare-sort U 0)
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(benchmark mathsat
:source { MathSat group }
:logic QF_UFLIA
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
+; COMMAND-LINE: --decision=justification
+; EXPECT: unsat
+
(benchmark pp_regfile.smt
:source {
Translated from old SVC processor verification benchmarks. Contact Clark
+++ /dev/null
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
sys.exit('"{}" must be *.cvc or *.smt or *.smt2 or *.p or *.sy'.format(
benchmark_basename))
- # If there is an ".expect" file for the benchmark, read the metadata
- # from there, otherwise from the benchmark file.
- metadata_filename = benchmark_path + '.expect'
- if os.path.isfile(metadata_filename):
- comment_char = '%'
- else:
- metadata_filename = benchmark_path
-
- metadata_lines = None
- with open(metadata_filename, 'r') as metadata_file:
- metadata_lines = metadata_file.readlines()
-
- benchmark_content = None
- if metadata_filename == benchmark_path:
- benchmark_content = ''.join(metadata_lines)
- else:
- with open(benchmark_path, 'r') as benchmark_file:
- benchmark_content = benchmark_file.read()
+ benchmark_lines = None
+ with open(benchmark_path, 'r') as benchmark_file:
+ benchmark_lines = benchmark_file.readlines()
+ benchmark_content = ''.join(benchmark_lines)
# Extract the metadata for the benchmark.
scrubber = None
expected_exit_status = None
command_lines = []
requires = []
- for line in metadata_lines:
+ for line in benchmark_lines:
# Skip lines that do not start with a comment character.
if line[0] != comment_char:
continue
projects / cvc5.git / commitdiff