From 8633358b0dcf298090431869a64f67dbd5cc232f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 19 Jul 2024 17:38:54 +0200 Subject: [PATCH] Add a test --- tests/dune.inc | 249 +++++++++++++++++++++++++++++++++++++ tests/issues/1170.expected | 2 + tests/issues/1170.smt2 | 6 + 3 files changed, 257 insertions(+) create mode 100644 tests/issues/1170.expected create mode 100644 tests/issues/1170.smt2 diff --git a/tests/dune.inc b/tests/dune.inc index a647e7540..45a4455ad 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -180334,6 +180334,255 @@ (package alt-ergo) (action (diff 340.expected 340_fpa.output))) + (rule + (target 1170_ci_cdcl_no_minimal_bj.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) + (rule + (deps 1170_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_cdcl_no_minimal_bj.output))) + (rule + (target 1170_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps 1170_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target 1170_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps 1170_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_no_tableaux_cdcl_in_instantiation.output))) + (rule + (target 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) + (rule + (deps 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target 1170_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (deps 1170_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target 1170_cdcl.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) + (rule + (deps 1170_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1170.expected 1170_cdcl.output))) + (rule + (target 1170_tableaux_cdcl.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) + (rule + (deps 1170_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1170.expected 1170_tableaux_cdcl.output))) + (rule + (target 1170_tableaux.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps 1170_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1170.expected 1170_tableaux.output))) + (rule + (target 1170_dolmen.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps 1170_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1170.expected 1170_dolmen.output))) + (rule + (target 1170_fpa.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) + (rule + (deps 1170_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1170.expected 1170_fpa.output))) (rule (target 1163.models_dolmen.output) (deps (:input 1163.models.smt2)) diff --git a/tests/issues/1170.expected b/tests/issues/1170.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/issues/1170.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/issues/1170.smt2 b/tests/issues/1170.smt2 new file mode 100644 index 000000000..94ab438f8 --- /dev/null +++ b/tests/issues/1170.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_BV) +(declare-const A (_ BitVec 2)) +(declare-const B (_ BitVec 1)) +(declare-const C (_ BitVec 3)) +(assert (= (bvmul (_ bv3 4) (concat A (concat #b0 B))) (concat C #b1))) +(check-sat)