From 4332a8cbecc777bfb32b6f099be3c2e58147a92f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 12 Nov 2020 12:46:46 +0100
Subject: [PATCH] We got back all the tests of Popop
except the one about efficiency with learning
---
src_colibri2/popop_lib/debug.ml | 1 +
.../generate_tests/generate_dune_tests.ml | 2 +-
src_colibri2/tests/solve/dimacs/sat/dune.inc | 22 +-
.../tests/solve/dimacs/unsat/dune.inc | 12 +-
.../sat/arith_CombiRepr_normalize.smt2 | 0
.../sat/arith_conflict_add_disequality.smt2 | 0
.../solve/smt_lra}/sat/arith_conpoly.smt2 | 0
.../arith_decide_must_test_is_dis_equal.smt2 | 0
.../sat/arith_init_always_merge_itself.smt2 | 0
.../arith_init_and_propa_must_be_ordered.smt2 | 0
.../solve/smt_lra}/sat/arith_merge_case1.smt2 | 0
.../smt_lra}/sat/arith_merge_case_4_bis.smt2 | 0
...rith_merge_itself_coef_of_repr_is_one.smt2 | 0
.../sat/arith_merge_itself_last_case.smt2 | 0
.../arith_merge_itself_pivot_not_in_p12.smt2 | 0
.../sat/arith_merge_must_use_find.smt2 | 0
.../smt_lra}/sat/arith_mult_explication.smt2 | 2 +-
.../arith_mult_not_linear_in_conflict.smt2 | 0
.../sat/arith_normalize_use_find_def.smt2 | 0
.../solve/smt_lra}/sat/arith_own_repr.smt2 | 0
.../solve/smt_lra}/sat/arith_propacl.smt2 | 0
.../sat/arith_subst_and_conflict_add.smt2 | 0
.../sat/attach_only_when_dom_present.smt2 | 0
src_colibri2/tests/solve/smt_lra/sat/dune.inc | 56 +-
.../solve/smt_lra}/sat/init_not_repr.smt2 | 0
.../sat/sem_invariant_in_learnt_dec.smt2 | 8 +-
.../smt_lra}/sat/solver_add_pexp_cl.smt2 | 0
.../solver_arith_homogeneous_dist_sign.smt2 | 0
.../sat/solver_merge_itself_repr_inside.smt2 | 0
.../solver_set_pending_merge_expsameexp.smt2 | 0
.../sat/solver_subst_eventdom_find.smt2 | 0
.../smt_lra}/unsat/arith_ExpMult_by_zero.smt2 | 0
.../smt_lra}/unsat/arith_merge_case2.smt2 | 0
src_colibri2/tests/solve/smt_lra/unsat/dune | 8 +
.../tests/solve/smt_lra/unsat/dune.inc | 9 +
.../unsat/solver_merge_itself_repr_empty.smt2 | 0
.../unsat/solver_set_sem_merge_sign.smt2 | 0
.../solve/smt_uf}/sat/and_propa_bcp.dmt2 | 0
.../smt_uf}/sat/bcp_dont_like_duplicate.smt2 | 0
.../solve/smt_uf}/sat/bool_not_propa.smt2 | 0
.../tests/solve/smt_uf}/sat/boolexpup.smt2 | 0
.../smt_uf}/sat/clause_normalization.smt2 | 0
.../tests/solve/smt_uf}/sat/clmerge.smt2 | 0
.../sat/conflict_complete_needed_cl.smt2 | 0
.../solve/smt_uf}/sat/directdom_not.smt2 | 0
.../smt_uf}/sat/dis_dom_before_first_age.smt2 | 0
.../solve/smt_uf}/sat/dom_merge_equality.smt2 | 0
src_colibri2/tests/solve/smt_uf/sat/dune.inc | 42 +-
.../tests/solve/smt_uf}/sat/equality.smt2 | 0
.../solve/smt_uf}/sat/equality_condis.smt2 | 0
.../solve/smt_uf}/sat/equality_get_sem.smt2 | 0
.../solve/smt_uf}/sat/exp_sem_equality.smt2 | 0
.../smt_uf}/sat/explimit_cl_equality.smt2 | 0
.../tests/solve/smt_uf}/sat/implication.smt2 | 0
.../smt_uf}/sat/intmap_set_disjoint.smt2 | 0
.../smt_uf}/sat/is_equal_not_propagated.smt2 | 0
.../tests/solve/smt_uf}/sat/ite_sem_bool.smt2 | 0
.../solve/smt_uf}/sat/polyeq_genequality.smt2 | 0
.../smt_uf}/sat/substupfalse_equality.smt2 | 0
.../tests/solve/smt_uf/unsat/dune.inc | 24 +-
.../get_repr_at__instead_of__equal_CRepr.smt2 | 0
.../smt_uf}/unsat/polyeq_genequality.smt2 | 0
src_colibri2/theories/LRA/LRA.ml | 3 +-
tests/dimacs/aim/aim-100-1_6-no-1.cnf | 2 +-
tests/dimacs/sat/anomaly_agetooold.cnf | 15 -
tests/dimacs/sat/anomaly_agetooold2.cnf | 32 --
tests/dimacs/sat/assertion_fail.cnf | 2 -
tests/dimacs/sat/fuzzing1.cnf | 17 -
tests/dimacs/sat/fuzzing2.cnf | 11 -
tests/dimacs/sat/par8-1-c.cnf | 530 ------------------
tests/dimacs/sat/pigeon-2.cnf | 24 -
tests/dimacs/sat/pigeon-3.cnf | 37 --
tests/dimacs/sat/pigeon-4.cnf | 60 --
tests/dimacs/sat/quinn.cnf | 21 -
tests/dimacs/sat/simple_v3_c2.cnf | 5 -
tests/dimacs/unsat/anomaly_agetooold.cnf | 22 -
tests/dimacs/unsat/modus_ponens.cnf | 6 -
tests/dimacs/unsat/pigeon-1.cnf | 19 -
tests/dimacs/unsat/pigeon-2.cnf | 25 -
tests/dimacs/unsat/pigeon-3.cnf | 38 --
tests/dimacs/unsat/pigeon-4.cnf | 61 --
tests/smtlib2/lra/sat/arith_merge_case_4.smt2 | 14 -
tests/smtlib2/lra/sat/arith_zero_dom.smt2 | 11 -
.../uf/unsat/NEQ004_size4__decide_eq_us.smt2 | 23 -
tests/smtlib2/uf/unsat/distinct.smt2 | 10 -
tests/smtlib2/uf/unsat/eq_diamond2.smt2 | 20 -
tests/smtlib2/uf/unsat/equality_norm_set.smt2 | 12 -
tests/smtlib2/uf/unsat/xor.smt2 | 11 -
88 files changed, 153 insertions(+), 1064 deletions(-)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_CombiRepr_normalize.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_conflict_add_disequality.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_conpoly.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_decide_must_test_is_dis_equal.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_init_always_merge_itself.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_init_and_propa_must_be_ordered.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_merge_case1.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_merge_case_4_bis.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_merge_itself_coef_of_repr_is_one.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_merge_itself_last_case.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_merge_itself_pivot_not_in_p12.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_merge_must_use_find.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_mult_explication.smt2 (90%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_mult_not_linear_in_conflict.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_normalize_use_find_def.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_own_repr.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_propacl.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/arith_subst_and_conflict_add.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/attach_only_when_dom_present.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/init_not_repr.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/sem_invariant_in_learnt_dec.smt2 (95%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/solver_add_pexp_cl.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/solver_arith_homogeneous_dist_sign.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/solver_merge_itself_repr_inside.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/solver_set_pending_merge_expsameexp.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/sat/solver_subst_eventdom_find.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/unsat/arith_ExpMult_by_zero.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/unsat/arith_merge_case2.smt2 (100%)
create mode 100644 src_colibri2/tests/solve/smt_lra/unsat/dune
create mode 100644 src_colibri2/tests/solve/smt_lra/unsat/dune.inc
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/unsat/solver_merge_itself_repr_empty.smt2 (100%)
rename {tests/smtlib2/lra => src_colibri2/tests/solve/smt_lra}/unsat/solver_set_sem_merge_sign.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/and_propa_bcp.dmt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/bcp_dont_like_duplicate.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/bool_not_propa.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/boolexpup.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/clause_normalization.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/clmerge.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/conflict_complete_needed_cl.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/directdom_not.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/dis_dom_before_first_age.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/dom_merge_equality.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/equality.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/equality_condis.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/equality_get_sem.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/exp_sem_equality.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/explimit_cl_equality.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/implication.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/intmap_set_disjoint.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/is_equal_not_propagated.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/ite_sem_bool.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/polyeq_genequality.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/sat/substupfalse_equality.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/unsat/get_repr_at__instead_of__equal_CRepr.smt2 (100%)
rename {tests/smtlib2/uf => src_colibri2/tests/solve/smt_uf}/unsat/polyeq_genequality.smt2 (100%)
delete mode 100644 tests/dimacs/sat/anomaly_agetooold.cnf
delete mode 100644 tests/dimacs/sat/anomaly_agetooold2.cnf
delete mode 100644 tests/dimacs/sat/assertion_fail.cnf
delete mode 100644 tests/dimacs/sat/fuzzing1.cnf
delete mode 100644 tests/dimacs/sat/fuzzing2.cnf
delete mode 100644 tests/dimacs/sat/par8-1-c.cnf
delete mode 100644 tests/dimacs/sat/pigeon-2.cnf
delete mode 100644 tests/dimacs/sat/pigeon-3.cnf
delete mode 100644 tests/dimacs/sat/pigeon-4.cnf
delete mode 100644 tests/dimacs/sat/quinn.cnf
delete mode 100644 tests/dimacs/sat/simple_v3_c2.cnf
delete mode 100644 tests/dimacs/unsat/anomaly_agetooold.cnf
delete mode 100644 tests/dimacs/unsat/modus_ponens.cnf
delete mode 100644 tests/dimacs/unsat/pigeon-1.cnf
delete mode 100644 tests/dimacs/unsat/pigeon-2.cnf
delete mode 100644 tests/dimacs/unsat/pigeon-3.cnf
delete mode 100644 tests/dimacs/unsat/pigeon-4.cnf
delete mode 100644 tests/smtlib2/lra/sat/arith_merge_case_4.smt2
delete mode 100644 tests/smtlib2/lra/sat/arith_zero_dom.smt2
delete mode 100644 tests/smtlib2/uf/unsat/NEQ004_size4__decide_eq_us.smt2
delete mode 100644 tests/smtlib2/uf/unsat/distinct.smt2
delete mode 100644 tests/smtlib2/uf/unsat/eq_diamond2.smt2
delete mode 100644 tests/smtlib2/uf/unsat/equality_norm_set.smt2
delete mode 100644 tests/smtlib2/uf/unsat/xor.smt2
diff --git a/src_colibri2/popop_lib/debug.ml b/src_colibri2/popop_lib/debug.ml
index 01f313e3c..79c28e0f6 100644
--- a/src_colibri2/popop_lib/debug.ml
+++ b/src_colibri2/popop_lib/debug.ml
@@ -108,6 +108,7 @@ let real_dprintf ?nobox s =
Format.kfprintf
(fun fmt -> if box then begin
Format.pp_close_box fmt ();
+ Format.pp_print_flush fmt ();
end
)
!formatter s
diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
index 59da80597..717da2a3d 100644
--- a/src_colibri2/tests/generate_tests/generate_dune_tests.ml
+++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -3,7 +3,7 @@ let result = Sys.argv.(2)
let print_test cout file =
Printf.fprintf cout
- "(rule (action (with-stdout-to %s.res (run colibri2 --max-step 1000 %s))))\n"
+ "(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-step 1000 %%{dep:%s}))))\n"
file file;
Printf.fprintf cout
"(rule (alias runtest) (action (diff oracle %s.res)))\n"
diff --git a/src_colibri2/tests/solve/dimacs/sat/dune.inc b/src_colibri2/tests/solve/dimacs/sat/dune.inc
index e534f7ee2..84ef1d52e 100644
--- a/src_colibri2/tests/solve/dimacs/sat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/sat/dune.inc
@@ -1,23 +1,23 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run colibri2 --max-step 1000 anomaly_agetooold.cnf))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:anomaly_agetooold.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
-(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run colibri2 --max-step 1000 anomaly_agetooold2.cnf))))
+(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:anomaly_agetooold2.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold2.cnf.res)))
-(rule (action (with-stdout-to assertion_fail.cnf.res (run colibri2 --max-step 1000 assertion_fail.cnf))))
+(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:assertion_fail.cnf}))))
(rule (alias runtest) (action (diff oracle assertion_fail.cnf.res)))
-(rule (action (with-stdout-to fuzzing1.cnf.res (run colibri2 --max-step 1000 fuzzing1.cnf))))
+(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:fuzzing1.cnf}))))
(rule (alias runtest) (action (diff oracle fuzzing1.cnf.res)))
-(rule (action (with-stdout-to fuzzing2.cnf.res (run colibri2 --max-step 1000 fuzzing2.cnf))))
+(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:fuzzing2.cnf}))))
(rule (alias runtest) (action (diff oracle fuzzing2.cnf.res)))
-(rule (action (with-stdout-to par8-1-c.cnf.res (run colibri2 --max-step 1000 par8-1-c.cnf))))
+(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:par8-1-c.cnf}))))
(rule (alias runtest) (action (diff oracle par8-1-c.cnf.res)))
-(rule (action (with-stdout-to pigeon-2.cnf.res (run colibri2 --max-step 1000 pigeon-2.cnf))))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-2.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
-(rule (action (with-stdout-to pigeon-3.cnf.res (run colibri2 --max-step 1000 pigeon-3.cnf))))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-3.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
-(rule (action (with-stdout-to pigeon-4.cnf.res (run colibri2 --max-step 1000 pigeon-4.cnf))))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-4.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
-(rule (action (with-stdout-to quinn.cnf.res (run colibri2 --max-step 1000 quinn.cnf))))
+(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:quinn.cnf}))))
(rule (alias runtest) (action (diff oracle quinn.cnf.res)))
-(rule (action (with-stdout-to simple_v3_c2.cnf.res (run colibri2 --max-step 1000 simple_v3_c2.cnf))))
+(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:simple_v3_c2.cnf}))))
(rule (alias runtest) (action (diff oracle simple_v3_c2.cnf.res)))
diff --git a/src_colibri2/tests/solve/dimacs/unsat/dune.inc b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
index 71418ed37..95157f79e 100644
--- a/src_colibri2/tests/solve/dimacs/unsat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
@@ -1,13 +1,13 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run colibri2 --max-step 1000 anomaly_agetooold.cnf))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:anomaly_agetooold.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
-(rule (action (with-stdout-to modus_ponens.cnf.res (run colibri2 --max-step 1000 modus_ponens.cnf))))
+(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:modus_ponens.cnf}))))
(rule (alias runtest) (action (diff oracle modus_ponens.cnf.res)))
-(rule (action (with-stdout-to pigeon-1.cnf.res (run colibri2 --max-step 1000 pigeon-1.cnf))))
+(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-1.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-1.cnf.res)))
-(rule (action (with-stdout-to pigeon-2.cnf.res (run colibri2 --max-step 1000 pigeon-2.cnf))))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-2.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
-(rule (action (with-stdout-to pigeon-3.cnf.res (run colibri2 --max-step 1000 pigeon-3.cnf))))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-3.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
-(rule (action (with-stdout-to pigeon-4.cnf.res (run colibri2 --max-step 1000 pigeon-4.cnf))))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-4.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
diff --git a/tests/smtlib2/lra/sat/arith_CombiRepr_normalize.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_CombiRepr_normalize.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_CombiRepr_normalize.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_CombiRepr_normalize.smt2
diff --git a/tests/smtlib2/lra/sat/arith_conflict_add_disequality.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_conflict_add_disequality.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_conflict_add_disequality.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_conflict_add_disequality.smt2
diff --git a/tests/smtlib2/lra/sat/arith_conpoly.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_conpoly.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_conpoly.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_conpoly.smt2
diff --git a/tests/smtlib2/lra/sat/arith_decide_must_test_is_dis_equal.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_decide_must_test_is_dis_equal.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_decide_must_test_is_dis_equal.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_decide_must_test_is_dis_equal.smt2
diff --git a/tests/smtlib2/lra/sat/arith_init_always_merge_itself.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_init_always_merge_itself.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_init_always_merge_itself.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_init_always_merge_itself.smt2
diff --git a/tests/smtlib2/lra/sat/arith_init_and_propa_must_be_ordered.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_init_and_propa_must_be_ordered.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_init_and_propa_must_be_ordered.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_init_and_propa_must_be_ordered.smt2
diff --git a/tests/smtlib2/lra/sat/arith_merge_case1.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_merge_case1.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_merge_case1.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_merge_case1.smt2
diff --git a/tests/smtlib2/lra/sat/arith_merge_case_4_bis.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_merge_case_4_bis.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_merge_case_4_bis.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_merge_case_4_bis.smt2
diff --git a/tests/smtlib2/lra/sat/arith_merge_itself_coef_of_repr_is_one.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_merge_itself_coef_of_repr_is_one.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_merge_itself_coef_of_repr_is_one.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_merge_itself_coef_of_repr_is_one.smt2
diff --git a/tests/smtlib2/lra/sat/arith_merge_itself_last_case.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_merge_itself_last_case.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_merge_itself_last_case.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_merge_itself_last_case.smt2
diff --git a/tests/smtlib2/lra/sat/arith_merge_itself_pivot_not_in_p12.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_merge_itself_pivot_not_in_p12.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_merge_itself_pivot_not_in_p12.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_merge_itself_pivot_not_in_p12.smt2
diff --git a/tests/smtlib2/lra/sat/arith_merge_must_use_find.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_merge_must_use_find.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_merge_must_use_find.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_merge_must_use_find.smt2
diff --git a/tests/smtlib2/lra/sat/arith_mult_explication.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_mult_explication.smt2
similarity index 90%
rename from tests/smtlib2/lra/sat/arith_mult_explication.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_mult_explication.smt2
index c799fe419..9192d4fba 100644
--- a/tests/smtlib2/lra/sat/arith_mult_explication.smt2
+++ b/src_colibri2/tests/solve/smt_lra/sat/arith_mult_explication.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_LRA)
+(set-logic ALL)
(declare-fun v0 () Real)
(declare-fun b () Bool)
(assert
diff --git a/tests/smtlib2/lra/sat/arith_mult_not_linear_in_conflict.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_mult_not_linear_in_conflict.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_mult_not_linear_in_conflict.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_mult_not_linear_in_conflict.smt2
diff --git a/tests/smtlib2/lra/sat/arith_normalize_use_find_def.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_normalize_use_find_def.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_normalize_use_find_def.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_normalize_use_find_def.smt2
diff --git a/tests/smtlib2/lra/sat/arith_own_repr.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_own_repr.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_own_repr.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_own_repr.smt2
diff --git a/tests/smtlib2/lra/sat/arith_propacl.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_propacl.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_propacl.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_propacl.smt2
diff --git a/tests/smtlib2/lra/sat/arith_subst_and_conflict_add.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_subst_and_conflict_add.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/arith_subst_and_conflict_add.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/arith_subst_and_conflict_add.smt2
diff --git a/tests/smtlib2/lra/sat/attach_only_when_dom_present.smt2 b/src_colibri2/tests/solve/smt_lra/sat/attach_only_when_dom_present.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/attach_only_when_dom_present.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/attach_only_when_dom_present.smt2
diff --git a/src_colibri2/tests/solve/smt_lra/sat/dune.inc b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
index 0692f72d9..04891c6cb 100644
--- a/src_colibri2/tests/solve/smt_lra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
@@ -1,5 +1,57 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run colibri2 --max-step 1000 arith_merge_case_4.smt2))))
+(rule (action (with-stdout-to arith_CombiRepr_normalize.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_CombiRepr_normalize.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_CombiRepr_normalize.smt2.res)))
+(rule (action (with-stdout-to arith_conflict_add_disequality.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_conflict_add_disequality.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_conflict_add_disequality.smt2.res)))
+(rule (action (with-stdout-to arith_conpoly.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_conpoly.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_conpoly.smt2.res)))
+(rule (action (with-stdout-to arith_decide_must_test_is_dis_equal.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_decide_must_test_is_dis_equal.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_decide_must_test_is_dis_equal.smt2.res)))
+(rule (action (with-stdout-to arith_init_always_merge_itself.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_init_always_merge_itself.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_init_always_merge_itself.smt2.res)))
+(rule (action (with-stdout-to arith_init_and_propa_must_be_ordered.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_init_and_propa_must_be_ordered.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_init_and_propa_must_be_ordered.smt2.res)))
+(rule (action (with-stdout-to arith_merge_case1.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_merge_case1.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_merge_case1.smt2.res)))
+(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_merge_case_4.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case_4.smt2.res)))
-(rule (action (with-stdout-to arith_zero_dom.smt2.res (run colibri2 --max-step 1000 arith_zero_dom.smt2))))
+(rule (action (with-stdout-to arith_merge_case_4_bis.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_merge_case_4_bis.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_merge_case_4_bis.smt2.res)))
+(rule (action (with-stdout-to arith_merge_itself_coef_of_repr_is_one.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_merge_itself_coef_of_repr_is_one.smt2.res)))
+(rule (action (with-stdout-to arith_merge_itself_last_case.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_merge_itself_last_case.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_merge_itself_last_case.smt2.res)))
+(rule (action (with-stdout-to arith_merge_itself_pivot_not_in_p12.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_merge_itself_pivot_not_in_p12.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_merge_itself_pivot_not_in_p12.smt2.res)))
+(rule (action (with-stdout-to arith_merge_must_use_find.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_merge_must_use_find.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_merge_must_use_find.smt2.res)))
+(rule (action (with-stdout-to arith_mult_explication.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_mult_explication.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_mult_explication.smt2.res)))
+(rule (action (with-stdout-to arith_mult_not_linear_in_conflict.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_mult_not_linear_in_conflict.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_mult_not_linear_in_conflict.smt2.res)))
+(rule (action (with-stdout-to arith_normalize_use_find_def.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_normalize_use_find_def.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_normalize_use_find_def.smt2.res)))
+(rule (action (with-stdout-to arith_own_repr.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_own_repr.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_own_repr.smt2.res)))
+(rule (action (with-stdout-to arith_propacl.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_propacl.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_propacl.smt2.res)))
+(rule (action (with-stdout-to arith_subst_and_conflict_add.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_subst_and_conflict_add.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_subst_and_conflict_add.smt2.res)))
+(rule (action (with-stdout-to arith_zero_dom.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_zero_dom.smt2}))))
(rule (alias runtest) (action (diff oracle arith_zero_dom.smt2.res)))
+(rule (action (with-stdout-to attach_only_when_dom_present.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:attach_only_when_dom_present.smt2}))))
+(rule (alias runtest) (action (diff oracle attach_only_when_dom_present.smt2.res)))
+(rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:init_not_repr.smt2}))))
+(rule (alias runtest) (action (diff oracle init_not_repr.smt2.res)))
+(rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:sem_invariant_in_learnt_dec.smt2}))))
+(rule (alias runtest) (action (diff oracle sem_invariant_in_learnt_dec.smt2.res)))
+(rule (action (with-stdout-to solver_add_pexp_cl.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:solver_add_pexp_cl.smt2}))))
+(rule (alias runtest) (action (diff oracle solver_add_pexp_cl.smt2.res)))
+(rule (action (with-stdout-to solver_arith_homogeneous_dist_sign.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:solver_arith_homogeneous_dist_sign.smt2}))))
+(rule (alias runtest) (action (diff oracle solver_arith_homogeneous_dist_sign.smt2.res)))
+(rule (action (with-stdout-to solver_merge_itself_repr_inside.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:solver_merge_itself_repr_inside.smt2}))))
+(rule (alias runtest) (action (diff oracle solver_merge_itself_repr_inside.smt2.res)))
+(rule (action (with-stdout-to solver_set_pending_merge_expsameexp.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:solver_set_pending_merge_expsameexp.smt2}))))
+(rule (alias runtest) (action (diff oracle solver_set_pending_merge_expsameexp.smt2.res)))
+(rule (action (with-stdout-to solver_subst_eventdom_find.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:solver_subst_eventdom_find.smt2}))))
+(rule (alias runtest) (action (diff oracle solver_subst_eventdom_find.smt2.res)))
diff --git a/tests/smtlib2/lra/sat/init_not_repr.smt2 b/src_colibri2/tests/solve/smt_lra/sat/init_not_repr.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/init_not_repr.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/init_not_repr.smt2
diff --git a/tests/smtlib2/lra/sat/sem_invariant_in_learnt_dec.smt2 b/src_colibri2/tests/solve/smt_lra/sat/sem_invariant_in_learnt_dec.smt2
similarity index 95%
rename from tests/smtlib2/lra/sat/sem_invariant_in_learnt_dec.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/sem_invariant_in_learnt_dec.smt2
index c24a83be7..1459180fb 100644
--- a/tests/smtlib2/lra/sat/sem_invariant_in_learnt_dec.smt2
+++ b/src_colibri2/tests/solve/smt_lra/sat/sem_invariant_in_learnt_dec.smt2
@@ -1,10 +1,10 @@
-(set-logic QF_LRA)
+(set-logic ALL)
(declare-fun v0 () Real)
(assert
- (let ((?n1 8))
- (let ((?n2 5))
+ (let ((?n1 8.0))
+ (let ((?n2 5.0))
(let ((?n3 (* ?n1 ?n2)))
- (let ((?n4 0))
+ (let ((?n4 0.0))
(let ((?n5 (- ?n1)))
(let ((?n6 (* ?n4 ?n5)))
(let ((?n7 (* ?n1 ?n4)))
diff --git a/tests/smtlib2/lra/sat/solver_add_pexp_cl.smt2 b/src_colibri2/tests/solve/smt_lra/sat/solver_add_pexp_cl.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/solver_add_pexp_cl.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/solver_add_pexp_cl.smt2
diff --git a/tests/smtlib2/lra/sat/solver_arith_homogeneous_dist_sign.smt2 b/src_colibri2/tests/solve/smt_lra/sat/solver_arith_homogeneous_dist_sign.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/solver_arith_homogeneous_dist_sign.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/solver_arith_homogeneous_dist_sign.smt2
diff --git a/tests/smtlib2/lra/sat/solver_merge_itself_repr_inside.smt2 b/src_colibri2/tests/solve/smt_lra/sat/solver_merge_itself_repr_inside.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/solver_merge_itself_repr_inside.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/solver_merge_itself_repr_inside.smt2
diff --git a/tests/smtlib2/lra/sat/solver_set_pending_merge_expsameexp.smt2 b/src_colibri2/tests/solve/smt_lra/sat/solver_set_pending_merge_expsameexp.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/solver_set_pending_merge_expsameexp.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/solver_set_pending_merge_expsameexp.smt2
diff --git a/tests/smtlib2/lra/sat/solver_subst_eventdom_find.smt2 b/src_colibri2/tests/solve/smt_lra/sat/solver_subst_eventdom_find.smt2
similarity index 100%
rename from tests/smtlib2/lra/sat/solver_subst_eventdom_find.smt2
rename to src_colibri2/tests/solve/smt_lra/sat/solver_subst_eventdom_find.smt2
diff --git a/tests/smtlib2/lra/unsat/arith_ExpMult_by_zero.smt2 b/src_colibri2/tests/solve/smt_lra/unsat/arith_ExpMult_by_zero.smt2
similarity index 100%
rename from tests/smtlib2/lra/unsat/arith_ExpMult_by_zero.smt2
rename to src_colibri2/tests/solve/smt_lra/unsat/arith_ExpMult_by_zero.smt2
diff --git a/tests/smtlib2/lra/unsat/arith_merge_case2.smt2 b/src_colibri2/tests/solve/smt_lra/unsat/arith_merge_case2.smt2
similarity index 100%
rename from tests/smtlib2/lra/unsat/arith_merge_case2.smt2
rename to src_colibri2/tests/solve/smt_lra/unsat/arith_merge_case2.smt2
diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune b/src_colibri2/tests/solve/smt_lra/unsat/dune
new file mode 100644
index 000000000..9ca94f895
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_lra/unsat/dune
@@ -0,0 +1,8 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps (glob_files *.cnf) (glob_files *.smt2))
+ (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote)
+)
diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
new file mode 100644
index 000000000..99881a34e
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
@@ -0,0 +1,9 @@
+(rule (action (with-stdout-to oracle (echo "unsat\n"))))
+(rule (action (with-stdout-to arith_ExpMult_by_zero.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_ExpMult_by_zero.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_ExpMult_by_zero.smt2.res)))
+(rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_merge_case2.smt2}))))
+(rule (alias runtest) (action (diff oracle arith_merge_case2.smt2.res)))
+(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:solver_merge_itself_repr_empty.smt2}))))
+(rule (alias runtest) (action (diff oracle solver_merge_itself_repr_empty.smt2.res)))
+(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:solver_set_sem_merge_sign.smt2}))))
+(rule (alias runtest) (action (diff oracle solver_set_sem_merge_sign.smt2.res)))
diff --git a/tests/smtlib2/lra/unsat/solver_merge_itself_repr_empty.smt2 b/src_colibri2/tests/solve/smt_lra/unsat/solver_merge_itself_repr_empty.smt2
similarity index 100%
rename from tests/smtlib2/lra/unsat/solver_merge_itself_repr_empty.smt2
rename to src_colibri2/tests/solve/smt_lra/unsat/solver_merge_itself_repr_empty.smt2
diff --git a/tests/smtlib2/lra/unsat/solver_set_sem_merge_sign.smt2 b/src_colibri2/tests/solve/smt_lra/unsat/solver_set_sem_merge_sign.smt2
similarity index 100%
rename from tests/smtlib2/lra/unsat/solver_set_sem_merge_sign.smt2
rename to src_colibri2/tests/solve/smt_lra/unsat/solver_set_sem_merge_sign.smt2
diff --git a/tests/smtlib2/uf/sat/and_propa_bcp.dmt2 b/src_colibri2/tests/solve/smt_uf/sat/and_propa_bcp.dmt2
similarity index 100%
rename from tests/smtlib2/uf/sat/and_propa_bcp.dmt2
rename to src_colibri2/tests/solve/smt_uf/sat/and_propa_bcp.dmt2
diff --git a/tests/smtlib2/uf/sat/bcp_dont_like_duplicate.smt2 b/src_colibri2/tests/solve/smt_uf/sat/bcp_dont_like_duplicate.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/bcp_dont_like_duplicate.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/bcp_dont_like_duplicate.smt2
diff --git a/tests/smtlib2/uf/sat/bool_not_propa.smt2 b/src_colibri2/tests/solve/smt_uf/sat/bool_not_propa.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/bool_not_propa.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/bool_not_propa.smt2
diff --git a/tests/smtlib2/uf/sat/boolexpup.smt2 b/src_colibri2/tests/solve/smt_uf/sat/boolexpup.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/boolexpup.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/boolexpup.smt2
diff --git a/tests/smtlib2/uf/sat/clause_normalization.smt2 b/src_colibri2/tests/solve/smt_uf/sat/clause_normalization.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/clause_normalization.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/clause_normalization.smt2
diff --git a/tests/smtlib2/uf/sat/clmerge.smt2 b/src_colibri2/tests/solve/smt_uf/sat/clmerge.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/clmerge.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/clmerge.smt2
diff --git a/tests/smtlib2/uf/sat/conflict_complete_needed_cl.smt2 b/src_colibri2/tests/solve/smt_uf/sat/conflict_complete_needed_cl.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/conflict_complete_needed_cl.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/conflict_complete_needed_cl.smt2
diff --git a/tests/smtlib2/uf/sat/directdom_not.smt2 b/src_colibri2/tests/solve/smt_uf/sat/directdom_not.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/directdom_not.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/directdom_not.smt2
diff --git a/tests/smtlib2/uf/sat/dis_dom_before_first_age.smt2 b/src_colibri2/tests/solve/smt_uf/sat/dis_dom_before_first_age.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/dis_dom_before_first_age.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/dis_dom_before_first_age.smt2
diff --git a/tests/smtlib2/uf/sat/dom_merge_equality.smt2 b/src_colibri2/tests/solve/smt_uf/sat/dom_merge_equality.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/dom_merge_equality.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/dom_merge_equality.smt2
diff --git a/src_colibri2/tests/solve/smt_uf/sat/dune.inc b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
index 0b8d7662a..443f8b688 100644
--- a/src_colibri2/tests/solve/smt_uf/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
@@ -1,3 +1,43 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to bad_conflict.smt2.res (run colibri2 --max-step 1000 bad_conflict.smt2))))
+(rule (action (with-stdout-to bad_conflict.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:bad_conflict.smt2}))))
(rule (alias runtest) (action (diff oracle bad_conflict.smt2.res)))
+(rule (action (with-stdout-to bcp_dont_like_duplicate.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:bcp_dont_like_duplicate.smt2}))))
+(rule (alias runtest) (action (diff oracle bcp_dont_like_duplicate.smt2.res)))
+(rule (action (with-stdout-to bool_not_propa.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:bool_not_propa.smt2}))))
+(rule (alias runtest) (action (diff oracle bool_not_propa.smt2.res)))
+(rule (action (with-stdout-to boolexpup.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:boolexpup.smt2}))))
+(rule (alias runtest) (action (diff oracle boolexpup.smt2.res)))
+(rule (action (with-stdout-to clause_normalization.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:clause_normalization.smt2}))))
+(rule (alias runtest) (action (diff oracle clause_normalization.smt2.res)))
+(rule (action (with-stdout-to clmerge.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:clmerge.smt2}))))
+(rule (alias runtest) (action (diff oracle clmerge.smt2.res)))
+(rule (action (with-stdout-to conflict_complete_needed_cl.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:conflict_complete_needed_cl.smt2}))))
+(rule (alias runtest) (action (diff oracle conflict_complete_needed_cl.smt2.res)))
+(rule (action (with-stdout-to directdom_not.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:directdom_not.smt2}))))
+(rule (alias runtest) (action (diff oracle directdom_not.smt2.res)))
+(rule (action (with-stdout-to dis_dom_before_first_age.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:dis_dom_before_first_age.smt2}))))
+(rule (alias runtest) (action (diff oracle dis_dom_before_first_age.smt2.res)))
+(rule (action (with-stdout-to dom_merge_equality.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:dom_merge_equality.smt2}))))
+(rule (alias runtest) (action (diff oracle dom_merge_equality.smt2.res)))
+(rule (action (with-stdout-to equality.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:equality.smt2}))))
+(rule (alias runtest) (action (diff oracle equality.smt2.res)))
+(rule (action (with-stdout-to equality_condis.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:equality_condis.smt2}))))
+(rule (alias runtest) (action (diff oracle equality_condis.smt2.res)))
+(rule (action (with-stdout-to equality_get_sem.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:equality_get_sem.smt2}))))
+(rule (alias runtest) (action (diff oracle equality_get_sem.smt2.res)))
+(rule (action (with-stdout-to exp_sem_equality.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:exp_sem_equality.smt2}))))
+(rule (alias runtest) (action (diff oracle exp_sem_equality.smt2.res)))
+(rule (action (with-stdout-to explimit_cl_equality.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:explimit_cl_equality.smt2}))))
+(rule (alias runtest) (action (diff oracle explimit_cl_equality.smt2.res)))
+(rule (action (with-stdout-to implication.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:implication.smt2}))))
+(rule (alias runtest) (action (diff oracle implication.smt2.res)))
+(rule (action (with-stdout-to intmap_set_disjoint.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:intmap_set_disjoint.smt2}))))
+(rule (alias runtest) (action (diff oracle intmap_set_disjoint.smt2.res)))
+(rule (action (with-stdout-to is_equal_not_propagated.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:is_equal_not_propagated.smt2}))))
+(rule (alias runtest) (action (diff oracle is_equal_not_propagated.smt2.res)))
+(rule (action (with-stdout-to ite_sem_bool.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:ite_sem_bool.smt2}))))
+(rule (alias runtest) (action (diff oracle ite_sem_bool.smt2.res)))
+(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:polyeq_genequality.smt2}))))
+(rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res)))
+(rule (action (with-stdout-to substupfalse_equality.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:substupfalse_equality.smt2}))))
+(rule (alias runtest) (action (diff oracle substupfalse_equality.smt2.res)))
diff --git a/tests/smtlib2/uf/sat/equality.smt2 b/src_colibri2/tests/solve/smt_uf/sat/equality.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/equality.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/equality.smt2
diff --git a/tests/smtlib2/uf/sat/equality_condis.smt2 b/src_colibri2/tests/solve/smt_uf/sat/equality_condis.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/equality_condis.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/equality_condis.smt2
diff --git a/tests/smtlib2/uf/sat/equality_get_sem.smt2 b/src_colibri2/tests/solve/smt_uf/sat/equality_get_sem.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/equality_get_sem.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/equality_get_sem.smt2
diff --git a/tests/smtlib2/uf/sat/exp_sem_equality.smt2 b/src_colibri2/tests/solve/smt_uf/sat/exp_sem_equality.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/exp_sem_equality.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/exp_sem_equality.smt2
diff --git a/tests/smtlib2/uf/sat/explimit_cl_equality.smt2 b/src_colibri2/tests/solve/smt_uf/sat/explimit_cl_equality.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/explimit_cl_equality.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/explimit_cl_equality.smt2
diff --git a/tests/smtlib2/uf/sat/implication.smt2 b/src_colibri2/tests/solve/smt_uf/sat/implication.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/implication.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/implication.smt2
diff --git a/tests/smtlib2/uf/sat/intmap_set_disjoint.smt2 b/src_colibri2/tests/solve/smt_uf/sat/intmap_set_disjoint.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/intmap_set_disjoint.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/intmap_set_disjoint.smt2
diff --git a/tests/smtlib2/uf/sat/is_equal_not_propagated.smt2 b/src_colibri2/tests/solve/smt_uf/sat/is_equal_not_propagated.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/is_equal_not_propagated.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/is_equal_not_propagated.smt2
diff --git a/tests/smtlib2/uf/sat/ite_sem_bool.smt2 b/src_colibri2/tests/solve/smt_uf/sat/ite_sem_bool.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/ite_sem_bool.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/ite_sem_bool.smt2
diff --git a/tests/smtlib2/uf/sat/polyeq_genequality.smt2 b/src_colibri2/tests/solve/smt_uf/sat/polyeq_genequality.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/polyeq_genequality.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/polyeq_genequality.smt2
diff --git a/tests/smtlib2/uf/sat/substupfalse_equality.smt2 b/src_colibri2/tests/solve/smt_uf/sat/substupfalse_equality.smt2
similarity index 100%
rename from tests/smtlib2/uf/sat/substupfalse_equality.smt2
rename to src_colibri2/tests/solve/smt_uf/sat/substupfalse_equality.smt2
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
index 0fd7accf3..5e8a4d497 100644
--- a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
@@ -1,21 +1,25 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run colibri2 --max-step 1000 NEQ004_size4__decide_eq_us.smt2))))
+(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:NEQ004_size4__decide_eq_us.smt2}))))
(rule (alias runtest) (action (diff oracle NEQ004_size4__decide_eq_us.smt2.res)))
-(rule (action (with-stdout-to deltaed0.smt2.res (run colibri2 --max-step 1000 deltaed0.smt2))))
+(rule (action (with-stdout-to deltaed0.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:deltaed0.smt2}))))
(rule (alias runtest) (action (diff oracle deltaed0.smt2.res)))
-(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run colibri2 --max-step 1000 diff_to_value_for_bool.smt2))))
+(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:diff_to_value_for_bool.smt2}))))
(rule (alias runtest) (action (diff oracle diff_to_value_for_bool.smt2.res)))
-(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run colibri2 --max-step 1000 diff_value_substupfalse.smt2))))
+(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:diff_value_substupfalse.smt2}))))
(rule (alias runtest) (action (diff oracle diff_value_substupfalse.smt2.res)))
-(rule (action (with-stdout-to distinct.smt2.res (run colibri2 --max-step 1000 distinct.smt2))))
+(rule (action (with-stdout-to distinct.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:distinct.smt2}))))
(rule (alias runtest) (action (diff oracle distinct.smt2.res)))
-(rule (action (with-stdout-to eq_diamond2.smt2.res (run colibri2 --max-step 1000 eq_diamond2.smt2))))
+(rule (action (with-stdout-to eq_diamond2.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:eq_diamond2.smt2}))))
(rule (alias runtest) (action (diff oracle eq_diamond2.smt2.res)))
-(rule (action (with-stdout-to equality_norm_set.smt2.res (run colibri2 --max-step 1000 equality_norm_set.smt2))))
+(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:equality_norm_set.smt2}))))
(rule (alias runtest) (action (diff oracle equality_norm_set.smt2.res)))
-(rule (action (with-stdout-to many_distinct.smt2.res (run colibri2 --max-step 1000 many_distinct.smt2))))
+(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:get_repr_at__instead_of__equal_CRepr.smt2}))))
+(rule (alias runtest) (action (diff oracle get_repr_at__instead_of__equal_CRepr.smt2.res)))
+(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:many_distinct.smt2}))))
(rule (alias runtest) (action (diff oracle many_distinct.smt2.res)))
-(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run colibri2 --max-step 1000 polyeq_genequality_deltaed.smt2))))
+(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:polyeq_genequality.smt2}))))
+(rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res)))
+(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:polyeq_genequality_deltaed.smt2}))))
(rule (alias runtest) (action (diff oracle polyeq_genequality_deltaed.smt2.res)))
-(rule (action (with-stdout-to xor.smt2.res (run colibri2 --max-step 1000 xor.smt2))))
+(rule (action (with-stdout-to xor.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:xor.smt2}))))
(rule (alias runtest) (action (diff oracle xor.smt2.res)))
diff --git a/tests/smtlib2/uf/unsat/get_repr_at__instead_of__equal_CRepr.smt2 b/src_colibri2/tests/solve/smt_uf/unsat/get_repr_at__instead_of__equal_CRepr.smt2
similarity index 100%
rename from tests/smtlib2/uf/unsat/get_repr_at__instead_of__equal_CRepr.smt2
rename to src_colibri2/tests/solve/smt_uf/unsat/get_repr_at__instead_of__equal_CRepr.smt2
diff --git a/tests/smtlib2/uf/unsat/polyeq_genequality.smt2 b/src_colibri2/tests/solve/smt_uf/unsat/polyeq_genequality.smt2
similarity index 100%
rename from tests/smtlib2/uf/unsat/polyeq_genequality.smt2
rename to src_colibri2/tests/solve/smt_uf/unsat/polyeq_genequality.smt2
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index 84cdd0fd2..3b8411af0 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -353,9 +353,10 @@ module DaemonPropa = struct
];
let cl = (SE.node s) in
let add acc c cl =
+ let cl = Egraph.find d cl in
match Egraph.get_dom d dom_poly cl with
| None -> Polynome.add acc (Polynome.monome c cl)
- | Some p -> Polynome.add acc p
+ | Some p -> Polynome.x_p_cy acc c p
in
let p1 = add (add Polynome.zero c1 cl1) c2 cl2 in
Th.solve_one d cl p1
diff --git a/tests/dimacs/aim/aim-100-1_6-no-1.cnf b/tests/dimacs/aim/aim-100-1_6-no-1.cnf
index 0b72579b2..2e0e818eb 100644
--- a/tests/dimacs/aim/aim-100-1_6-no-1.cnf
+++ b/tests/dimacs/aim/aim-100-1_6-no-1.cnf
@@ -168,4 +168,4 @@ p cnf 100 160
-2 -53 -58 0
43 -45 -96 0
34 -45 -69 0
-63 -86 -98 0
\ No newline at end of file
+63 -86 -98 0
diff --git a/tests/dimacs/sat/anomaly_agetooold.cnf b/tests/dimacs/sat/anomaly_agetooold.cnf
deleted file mode 100644
index 61413cffb..000000000
--- a/tests/dimacs/sat/anomaly_agetooold.cnf
+++ /dev/null
@@ -1,15 +0,0 @@
-p cnf 15 14
-1 -2 0
-3 2 0
--1 4 0
-6 -1 0
--2 -6 0
-2 -1 8 0
--9 -8 0
-9 12 0
--7 -13 0
--14 0
--3 1 0
--12 -15 5 2 0
-11 10 0
--4 -5 0
diff --git a/tests/dimacs/sat/anomaly_agetooold2.cnf b/tests/dimacs/sat/anomaly_agetooold2.cnf
deleted file mode 100644
index 93ba09bb3..000000000
--- a/tests/dimacs/sat/anomaly_agetooold2.cnf
+++ /dev/null
@@ -1,32 +0,0 @@
-p cnf 31 31
-4 -3 0
-1 7 0
-8 6 0
--9 -10 -11 0
-9 10 0
--9 10 0
-9 -10 11 0
--7 11 0
--10 12 0
--13 14 0
-2 -15 0
--4 -16 0
--17 16 0
--18 17 0
-19 18 0
-21 -20 0
--22 -21 0
--23 -12 0
-24 23 0
-20 25 0
--26 -25 0
-13 27 0
--27 28 0
-29 -28 0
--5 30 0
-5 30 0
--31 -30 0
--19 -14 -2 0
-31 -29 0
-22 -24 0
-26 15 0
diff --git a/tests/dimacs/sat/assertion_fail.cnf b/tests/dimacs/sat/assertion_fail.cnf
deleted file mode 100644
index 56a8f3dbf..000000000
--- a/tests/dimacs/sat/assertion_fail.cnf
+++ /dev/null
@@ -1,2 +0,0 @@
-p cnf 36 1
-36 0
diff --git a/tests/dimacs/sat/fuzzing1.cnf b/tests/dimacs/sat/fuzzing1.cnf
deleted file mode 100644
index bf3dfc6f1..000000000
--- a/tests/dimacs/sat/fuzzing1.cnf
+++ /dev/null
@@ -1,17 +0,0 @@
-c generated by FuzzSAT
-p cnf 7 15
--1 -2 -3 0
-1 2 -3 0
--1 2 3 0
-1 -2 3 0
--4 -2 0
--4 2 0
-5 2 0
-5 -2 0
-6 -4 0
-6 5 0
-4 -5 -6 0
-7 -3 0
-7 6 0
-3 -6 -7 0
-7 0
diff --git a/tests/dimacs/sat/fuzzing2.cnf b/tests/dimacs/sat/fuzzing2.cnf
deleted file mode 100644
index 9facc9e4f..000000000
--- a/tests/dimacs/sat/fuzzing2.cnf
+++ /dev/null
@@ -1,11 +0,0 @@
-c generated by FuzzSAT
-p cnf 5 9
--1 -2 0
-1 -2 0
--3 -1 0
--3 2 0
-1 -2 3 0
--5 -3 0
--5 -4 0
-3 4 5 0
-5 0
diff --git a/tests/dimacs/sat/par8-1-c.cnf b/tests/dimacs/sat/par8-1-c.cnf
deleted file mode 100644
index 90a8ddb21..000000000
--- a/tests/dimacs/sat/par8-1-c.cnf
+++ /dev/null
@@ -1,530 +0,0 @@
-c FILE: par8-1-c.cnf
-c
-c SOURCE: James Crawford (jc@research.att.com)
-c
-c DESCRIPTION: Instance arises from the problem of learning the parity
-c function.
-c
-c parxx-y denotes a parity problem on xx bits. y is simply the
-c intance number.
-c
-c parxx-y-c denotes an instance identical to parxx-y except that
-c the instances have been simplified (to create an equivalent
-c problem).
-c
-c NOTE: Satisfiable (checked for 8 and 16 size instances. All
-c instances are satisfiable by construction)
-c
-c NOTE: Number of clauses corrected August 3, 1993
-c
-c Converted from tableau format Tue Aug 3 09:55:20 EDT 1993
-p cnf 64 254
- -2 1
- 0
- -3 -2
- 0
- -3 -2 -1
- 0
- 3 2 -1
- 0
- -3 2 1
- 0
- 3 -2 1
- 0
- -4 2
- 0
- -5 -4
- 0
- -5 -4 -2
- 0
- 5 4 -2
- 0
- -5 4 2
- 0
- 5 -4 2
- 0
- -6 4
- 0
- -7 -6
- 0
- -7 -6 -4
- 0
- 7 6 -4
- 0
- -7 6 4
- 0
- 7 -6 4
- 0
- -8 6
- 0
- -9 -8
- 0
- -9 -8 -6
- 0
- 9 8 -6
- 0
- -9 8 6
- 0
- 9 -8 6
- 0
- -10 8
- 0
- -11 -10
- 0
- -11 -10 -8
- 0
- 11 10 -8
- 0
- -11 10 8
- 0
- 11 -10 8
- 0
- -12 10
- 0
- -13 -12
- 0
- -13 -12 -10
- 0
- 13 12 -10
- 0
- -13 12 10
- 0
- 13 -12 10
- 0
- -14 12
- 0
- -15 -14
- 0
- -15 -14 -12
- 0
- 15 14 -12
- 0
- -15 14 12
- 0
- 15 -14 12
- 0
- -16 14
- 0
- -17 -16
- 0
- -17 -16 -14
- 0
- 17 16 -14
- 0
- -17 16 14
- 0
- 17 -16 14
- 0
- -18 16
- 0
- -19 -18
- 0
- -19 -18 -16
- 0
- 19 18 -16
- 0
- -19 18 16
- 0
- 19 -18 16
- 0
- -20 18
- 0
- -21 -20
- 0
- -21 -20 -18
- 0
- 21 20 -18
- 0
- -21 20 18
- 0
- 21 -20 18
- 0
- -22 20
- 0
- -23 -22
- 0
- -23 -22 -20
- 0
- 23 22 -20
- 0
- -23 22 20
- 0
- 23 -22 20
- 0
- -24 22
- 0
- -25 -24
- 0
- -25 -24 -22
- 0
- 25 24 -22
- 0
- -25 24 22
- 0
- 25 -24 22
- 0
- -26 24
- 0
- -27 -26
- 0
- -27 -26 -24
- 0
- 27 26 -24
- 0
- -27 26 24
- 0
- 27 -26 24
- 0
- -28 26
- 0
- -29 -28
- 0
- -29 -28 -26
- 0
- 29 28 -26
- 0
- -29 28 26
- 0
- 29 -28 26
- 0
- 28 -30
- 0
- -31 -30
- 0
- -31 -28 -30
- 0
- 31 -28 30
- 0
- -31 28 30
- 0
- 31 28 -30
- 0
- -33 -32 -3
- 0
- 33 32 -3
- 0
- -33 32 3
- 0
- 33 -32 3
- 0
- -35 -34 -32
- 0
- 35 34 -32
- 0
- -35 34 32
- 0
- 35 -34 32
- 0
- -37 -34 36
- 0
- 37 -34 -36
- 0
- -37 34 -36
- 0
- 37 34 36
- 0
- -39 -38 -5
- 0
- 39 38 -5
- 0
- -39 38 5
- 0
- 39 -38 5
- 0
- -35 -40 -38
- 0
- 35 40 -38
- 0
- -35 40 38
- 0
- 35 -40 38
- 0
- -42 -41 -40
- 0
- 42 41 -40
- 0
- -42 41 40
- 0
- 42 -41 40
- 0
- -36 -41 43
- 0
- 36 -41 -43
- 0
- -36 41 -43
- 0
- 36 41 43
- 0
- -44 -7 29
- 0
- 44 -7 -29
- 0
- 44 7 29
- 0
- -44 7 -29
- 0
- -33 -45 -44
- 0
- 33 45 -44
- 0
- -33 45 44
- 0
- 33 -45 44
- 0
- -37 -36 -45
- 0
- 37 36 -45
- 0
- -37 36 45
- 0
- 37 -36 45
- 0
- -37 -46 -9
- 0
- 37 46 -9
- 0
- -37 46 9
- 0
- 37 -46 9
- 0
- -36 -43 -46
- 0
- 36 43 -46
- 0
- -36 43 46
- 0
- 36 -43 46
- 0
- -39 -47 -11
- 0
- 39 47 -11
- 0
- -39 47 11
- 0
- 39 -47 11
- 0
- -33 -48 -47
- 0
- 33 48 -47
- 0
- -33 48 47
- 0
- 33 -48 47
- 0
- -37 -36 -48
- 0
- 37 36 -48
- 0
- -37 36 48
- 0
- 37 -36 48
- 0
- -39 -49 -13
- 0
- 39 49 -13
- 0
- -39 49 13
- 0
- 39 -49 13
- 0
- -33 -36 -49
- 0
- 33 36 -49
- 0
- -33 36 49
- 0
- 33 -36 49
- 0
- -50 -15 29
- 0
- 50 -15 -29
- 0
- 50 15 29
- 0
- -50 15 -29
- 0
- -35 -37 -50
- 0
- 35 37 -50
- 0
- -35 37 50
- 0
- 35 -37 50
- 0
- -39 -35 -17
- 0
- 39 35 -17
- 0
- -39 35 17
- 0
- 39 -35 17
- 0
- -39 -51 -19
- 0
- 39 51 -19
- 0
- -39 51 19
- 0
- 39 -51 19
- 0
- -35 -52 -51
- 0
- 35 52 -51
- 0
- -35 52 51
- 0
- 35 -52 51
- 0
- -37 -52 42
- 0
- 37 -52 -42
- 0
- -37 52 -42
- 0
- 37 52 42
- 0
- -53 -21 29
- 0
- 53 -21 -29
- 0
- 53 21 29
- 0
- -53 21 -29
- 0
- -33 -54 -53
- 0
- 33 54 -53
- 0
- -33 54 53
- 0
- 33 -54 53
- 0
- -35 -54 42
- 0
- 35 -54 -42
- 0
- -35 54 -42
- 0
- 35 54 42
- 0
- -33 -23 42
- 0
- 33 -23 -42
- 0
- -33 23 -42
- 0
- 33 23 42
- 0
- -55 -25 29
- 0
- 55 -25 -29
- 0
- 55 25 29
- 0
- -55 25 -29
- 0
- -33 -56 -55
- 0
- 33 56 -55
- 0
- -33 56 55
- 0
- 33 -56 55
- 0
- -35 -56 36
- 0
- 35 -56 -36
- 0
- -35 56 -36
- 0
- 35 56 36
- 0
- -39 -57 -27
- 0
- 39 57 -27
- 0
- -39 57 27
- 0
- 39 -57 27
- 0
- -58 -57 29
- 0
- 58 -57 -29
- 0
- 58 57 29
- 0
- -58 57 -29
- 0
- -35 -59 -58
- 0
- 35 59 -58
- 0
- -35 59 58
- 0
- 35 -59 58
- 0
- -37 -59 -36
- 0
- 37 -59 36
- 0
- -37 59 36
- 0
- 37 59 -36
- 0
- -37 -60 -31
- 0
- 37 60 -31
- 0
- -37 60 31
- 0
- 37 -60 31
- 0
- -42 -61 -60
- 0
- 42 61 -60
- 0
- -42 61 60
- 0
- 42 -61 60
- 0
- -36 -61 43
- 0
- 36 -61 -43
- 0
- -36 61 -43
- 0
- 36 61 43
- 0
- -39 -62 -30
- 0
- 39 62 -30
- 0
- -39 62 30
- 0
- 39 -62 30
- 0
- -33 -63 -62
- 0
- 33 63 -62
- 0
- -33 63 62
- 0
- 33 -63 62
- 0
- -42 -64 -63
- 0
- 42 64 -63
- 0
- -42 64 63
- 0
- 42 -64 63
- 0
- -36 -64 -43
- 0
- 36 -64 43
- 0
- -36 64 43
- 0
- 36 64 -43
- 0
-
diff --git a/tests/dimacs/sat/pigeon-2.cnf b/tests/dimacs/sat/pigeon-2.cnf
deleted file mode 100644
index 4fea8d909..000000000
--- a/tests/dimacs/sat/pigeon-2.cnf
+++ /dev/null
@@ -1,24 +0,0 @@
-c pigeon-2: placing 3 pigeons into 2 holes
-c
-c File generated by 'pigeonhole', (c) Tjark Weber
-c
-c The SAT encoding of this problem is very straightforward. For each pigeon i
-c and each hole j we have a variable x_{n*(i-1)+j} which means that pigeon i
-c is placed in hole j. Then we have n+1 clauses which say that a pigeon has
-c to be placed in some hole. Then for each hole we have a set of clauses
-c ensuring that only one single pigeon is placed into that hole.
-c
-c This encoding leads to a total of (n+1) * n propositional variables and
-c (n+1) + n * (n * (n+1) / 2) clauses.
-c
-c The resulting SAT problem is unsatisfiable.
-c
-p cnf 6 9
-1 2 0
-3 4 0
-5 6 0
--1 -3 0
--1 -5 0
--3 -5 0
--2 -4 0
--2 -6 0
diff --git a/tests/dimacs/sat/pigeon-3.cnf b/tests/dimacs/sat/pigeon-3.cnf
deleted file mode 100644
index 4f2fd41d8..000000000
--- a/tests/dimacs/sat/pigeon-3.cnf
+++ /dev/null
@@ -1,37 +0,0 @@
-c pigeon-3: placing 4 pigeons into 3 holes
-c
-c File generated by 'pigeonhole', (c) Tjark Weber
-c
-c The SAT encoding of this problem is very straightforward. For each pigeon i
-c and each hole j we have a variable x_{n*(i-1)+j} which means that pigeon i
-c is placed in hole j. Then we have n+1 clauses which say that a pigeon has
-c to be placed in some hole. Then for each hole we have a set of clauses
-c ensuring that only one single pigeon is placed into that hole.
-c
-c This encoding leads to a total of (n+1) * n propositional variables and
-c (n+1) + n * (n * (n+1) / 2) clauses.
-c
-c The resulting SAT problem is unsatisfiable.
-c
-p cnf 12 22
-1 2 3 0
-4 5 6 0
-10 11 12 0
--1 -4 0
--1 -7 0
--1 -10 0
--4 -7 0
--4 -10 0
--7 -10 0
--2 -5 0
--2 -8 0
--2 -11 0
--5 -8 0
--5 -11 0
--8 -11 0
--3 -6 0
--3 -9 0
--3 -12 0
--6 -9 0
--6 -12 0
--9 -12 0
diff --git a/tests/dimacs/sat/pigeon-4.cnf b/tests/dimacs/sat/pigeon-4.cnf
deleted file mode 100644
index 690fbe4a8..000000000
--- a/tests/dimacs/sat/pigeon-4.cnf
+++ /dev/null
@@ -1,60 +0,0 @@
-c pigeon-4: placing 5 pigeons into 4 holes
-c
-c File generated by 'pigeonhole', (c) Tjark Weber
-c
-c The SAT encoding of this problem is very straightforward. For each pigeon i
-c and each hole j we have a variable x_{n*(i-1)+j} which means that pigeon i
-c is placed in hole j. Then we have n+1 clauses which say that a pigeon has
-c to be placed in some hole. Then for each hole we have a set of clauses
-c ensuring that only one single pigeon is placed into that hole.
-c
-c This encoding leads to a total of (n+1) * n propositional variables and
-c (n+1) + n * (n * (n+1) / 2) clauses.
-c
-c The resulting SAT problem is unsatisfiable.
-c
-p cnf 20 45
-1 2 3 4 0
-5 6 7 8 0
-9 10 11 12 0
-13 14 15 16 0
-17 18 19 20 0
--1 -5 0
--1 -9 0
--1 -13 0
--1 -17 0
--5 -9 0
--5 -13 0
--5 -17 0
--9 -13 0
--9 -17 0
--13 -17 0
--2 -6 0
--2 -10 0
--2 -14 0
--2 -18 0
--6 -10 0
--6 -14 0
--6 -18 0
--10 -14 0
--10 -18 0
--14 -18 0
--3 -7 0
--3 -11 0
--3 -15 0
--3 -19 0
--7 -11 0
--7 -15 0
--7 -19 0
--11 -15 0
--11 -19 0
--15 -19 0
--4 -8 0
--4 -12 0
--4 -16 0
--4 -20 0
--8 -12 0
--8 -16 0
--8 -20 0
--12 -16 0
--16 -20 0
diff --git a/tests/dimacs/sat/quinn.cnf b/tests/dimacs/sat/quinn.cnf
deleted file mode 100644
index 9c662227a..000000000
--- a/tests/dimacs/sat/quinn.cnf
+++ /dev/null
@@ -1,21 +0,0 @@
-c quinn.cnf
-c
-p cnf 16 18
- 1 2 0
- -2 -4 0
- 3 4 0
- -4 -5 0
- 5 -6 0
- 6 -7 0
- 6 7 0
- 7 -16 0
- 8 -9 0
- -8 -14 0
- 9 10 0
- 9 -10 0
--10 -11 0
- 10 12 0
- 11 12 0
- 13 14 0
- 14 -15 0
- 15 16 0
diff --git a/tests/dimacs/sat/simple_v3_c2.cnf b/tests/dimacs/sat/simple_v3_c2.cnf
deleted file mode 100644
index 93f36fcb4..000000000
--- a/tests/dimacs/sat/simple_v3_c2.cnf
+++ /dev/null
@@ -1,5 +0,0 @@
-c simple_v3_c2.cnf
-c
-p cnf 3 2
-1 -3 0
-2 3 -1 0
diff --git a/tests/dimacs/unsat/anomaly_agetooold.cnf b/tests/dimacs/unsat/anomaly_agetooold.cnf
deleted file mode 100644
index 5bb5254c5..000000000
--- a/tests/dimacs/unsat/anomaly_agetooold.cnf
+++ /dev/null
@@ -1,22 +0,0 @@
-p cnf 20 21
-3 -2 0
-1 2 0
-4 -5 0
-6 4 0
--6 7 0
--8 -7 0
-8 -9 0
-10 9 0
-12 11 0
-13 -2 0
--1 -14 0
-14 -12 15 0
--7 16 0
-17 -12 0
-4 -13 18 0
--11 19 0
--18 -20 0
--4 -17 0
--16 -15 0
--19 -11 0
--10 20 0
diff --git a/tests/dimacs/unsat/modus_ponens.cnf b/tests/dimacs/unsat/modus_ponens.cnf
deleted file mode 100644
index 9ee720c86..000000000
--- a/tests/dimacs/unsat/modus_ponens.cnf
+++ /dev/null
@@ -1,6 +0,0 @@
-c simple_v3_c2.cnf
-c
-p cnf 2 3
-1 0
--1 2 0
--2 0
diff --git a/tests/dimacs/unsat/pigeon-1.cnf b/tests/dimacs/unsat/pigeon-1.cnf
deleted file mode 100644
index c27f94a3d..000000000
--- a/tests/dimacs/unsat/pigeon-1.cnf
+++ /dev/null
@@ -1,19 +0,0 @@
-c pigeon-1: placing 2 pigeons into 1 holes
-c
-c File generated by 'pigeonhole', (c) Tjark Weber
-c
-c The SAT encoding of this problem is very straightforward. For each pigeon i
-c and each hole j we have a variable x_{n*(i-1)+j} which means that pigeon i
-c is placed in hole j. Then we have n+1 clauses which say that a pigeon has
-c to be placed in some hole. Then for each hole we have a set of clauses
-c ensuring that only one single pigeon is placed into that hole.
-c
-c This encoding leads to a total of (n+1) * n propositional variables and
-c (n+1) + n * (n * (n+1) / 2) clauses.
-c
-c The resulting SAT problem is unsatisfiable.
-c
-p cnf 2 3
-1 0
-2 0
--1 -2 0
diff --git a/tests/dimacs/unsat/pigeon-2.cnf b/tests/dimacs/unsat/pigeon-2.cnf
deleted file mode 100644
index b46ad69c8..000000000
--- a/tests/dimacs/unsat/pigeon-2.cnf
+++ /dev/null
@@ -1,25 +0,0 @@
-c pigeon-2: placing 3 pigeons into 2 holes
-c
-c File generated by 'pigeonhole', (c) Tjark Weber
-c
-c The SAT encoding of this problem is very straightforward. For each pigeon i
-c and each hole j we have a variable x_{n*(i-1)+j} which means that pigeon i
-c is placed in hole j. Then we have n+1 clauses which say that a pigeon has
-c to be placed in some hole. Then for each hole we have a set of clauses
-c ensuring that only one single pigeon is placed into that hole.
-c
-c This encoding leads to a total of (n+1) * n propositional variables and
-c (n+1) + n * (n * (n+1) / 2) clauses.
-c
-c The resulting SAT problem is unsatisfiable.
-c
-p cnf 6 9
-1 2 0
-3 4 0
-5 6 0
--1 -3 0
--1 -5 0
--3 -5 0
--2 -4 0
--2 -6 0
--4 -6 0
diff --git a/tests/dimacs/unsat/pigeon-3.cnf b/tests/dimacs/unsat/pigeon-3.cnf
deleted file mode 100644
index 86113f2d5..000000000
--- a/tests/dimacs/unsat/pigeon-3.cnf
+++ /dev/null
@@ -1,38 +0,0 @@
-c pigeon-3: placing 4 pigeons into 3 holes
-c
-c File generated by 'pigeonhole', (c) Tjark Weber
-c
-c The SAT encoding of this problem is very straightforward. For each pigeon i
-c and each hole j we have a variable x_{n*(i-1)+j} which means that pigeon i
-c is placed in hole j. Then we have n+1 clauses which say that a pigeon has
-c to be placed in some hole. Then for each hole we have a set of clauses
-c ensuring that only one single pigeon is placed into that hole.
-c
-c This encoding leads to a total of (n+1) * n propositional variables and
-c (n+1) + n * (n * (n+1) / 2) clauses.
-c
-c The resulting SAT problem is unsatisfiable.
-c
-p cnf 12 22
-1 2 3 0
-4 5 6 0
-7 8 9 0
-10 11 12 0
--1 -4 0
--1 -7 0
--1 -10 0
--4 -7 0
--4 -10 0
--7 -10 0
--2 -5 0
--2 -8 0
--2 -11 0
--5 -8 0
--5 -11 0
--8 -11 0
--3 -6 0
--3 -9 0
--3 -12 0
--6 -9 0
--6 -12 0
--9 -12 0
diff --git a/tests/dimacs/unsat/pigeon-4.cnf b/tests/dimacs/unsat/pigeon-4.cnf
deleted file mode 100644
index 436656c8c..000000000
--- a/tests/dimacs/unsat/pigeon-4.cnf
+++ /dev/null
@@ -1,61 +0,0 @@
-c pigeon-4: placing 5 pigeons into 4 holes
-c
-c File generated by 'pigeonhole', (c) Tjark Weber
-c
-c The SAT encoding of this problem is very straightforward. For each pigeon i
-c and each hole j we have a variable x_{n*(i-1)+j} which means that pigeon i
-c is placed in hole j. Then we have n+1 clauses which say that a pigeon has
-c to be placed in some hole. Then for each hole we have a set of clauses
-c ensuring that only one single pigeon is placed into that hole.
-c
-c This encoding leads to a total of (n+1) * n propositional variables and
-c (n+1) + n * (n * (n+1) / 2) clauses.
-c
-c The resulting SAT problem is unsatisfiable.
-c
-p cnf 20 45
-1 2 3 4 0
-5 6 7 8 0
-9 10 11 12 0
-13 14 15 16 0
-17 18 19 20 0
--1 -5 0
--1 -9 0
--1 -13 0
--1 -17 0
--5 -9 0
--5 -13 0
--5 -17 0
--9 -13 0
--9 -17 0
--13 -17 0
--2 -6 0
--2 -10 0
--2 -14 0
--2 -18 0
--6 -10 0
--6 -14 0
--6 -18 0
--10 -14 0
--10 -18 0
--14 -18 0
--3 -7 0
--3 -11 0
--3 -15 0
--3 -19 0
--7 -11 0
--7 -15 0
--7 -19 0
--11 -15 0
--11 -19 0
--15 -19 0
--4 -8 0
--4 -12 0
--4 -16 0
--4 -20 0
--8 -12 0
--8 -16 0
--8 -20 0
--12 -16 0
--12 -20 0
--16 -20 0
diff --git a/tests/smtlib2/lra/sat/arith_merge_case_4.smt2 b/tests/smtlib2/lra/sat/arith_merge_case_4.smt2
deleted file mode 100644
index 94b0337eb..000000000
--- a/tests/smtlib2/lra/sat/arith_merge_case_4.smt2
+++ /dev/null
@@ -1,14 +0,0 @@
-(set-logic QF_LRA)
-(declare-fun z () Real)
-(assert
- (let ((?3 3))
- (let ((?n2 (+ z ?3)))
- (let ((?2 2))
- (let ((?n4 (= ?n2 ?2)))
- (let ((?n5 (= z ?n2)))
- (let ((?n7 (not ?n5)))
- (let ((?n8 (and ?n4 ?n7)))
- (let ((?n9 (not ?n8))) ?n9
-)))))))))
-(check-sat)
-(exit)
diff --git a/tests/smtlib2/lra/sat/arith_zero_dom.smt2 b/tests/smtlib2/lra/sat/arith_zero_dom.smt2
deleted file mode 100644
index 86b63aa8e..000000000
--- a/tests/smtlib2/lra/sat/arith_zero_dom.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-(set-logic QF_LRA)
-(declare-fun v2 () Real)
-(declare-fun v1 () Real)
-(declare-fun b () Bool)
-(assert
- (let ((?1 1) (?0 0))
- (let ((?ite (ite b ?0 ?1)))
- (let ((?n7 (= ?1 ?ite))) ?n7
-))))
-(check-sat)
-(exit)
diff --git a/tests/smtlib2/uf/unsat/NEQ004_size4__decide_eq_us.smt2 b/tests/smtlib2/uf/unsat/NEQ004_size4__decide_eq_us.smt2
deleted file mode 100644
index 1dd30a3ad..000000000
--- a/tests/smtlib2/uf/unsat/NEQ004_size4__decide_eq_us.smt2
+++ /dev/null
@@ -1,23 +0,0 @@
-(set-logic QF_UF)
-(set-info :status unknown)
-(declare-sort U 0)
-(declare-fun c15 () U)
-(declare-fun c_3 () U)
-(declare-fun c_2 () U)
-(declare-fun p8 ( U) Bool)
-(declare-fun c11 () U)
-(declare-fun c13 () U)
-(declare-fun c14 () U)
-(assert
- (let ((?n2 (p8 c_2)))
- (let ((?n3 (not ?n2)))
- (let ((?n4 (p8 c_3)))
- (let ((?n5 (not ?n4)))
- (let ((?n8 (p8 c15)))
- (let ((?n10 (= c_2 c15)))
- (let ((?n11 (= c_3 c15)))
- (let ((?n12 (or ?n10 ?n11)))
- (let ((?n13 (and ?n3 ?n5 ?n8 ?n12))) ?n13
-))))))))))
-(check-sat)
-(exit)
diff --git a/tests/smtlib2/uf/unsat/distinct.smt2 b/tests/smtlib2/uf/unsat/distinct.smt2
deleted file mode 100644
index c0640415f..000000000
--- a/tests/smtlib2/uf/unsat/distinct.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-(set-logic QF_UF)
-(declare-sort S0 0)
-(assert
- (let ((?n1 true))
- (let ((?n2 false))
- (let ((?n3 (xor ?n1 ?n2)))
- (let ((?n4 (xor ?n1 ?n3))) ?n4
-)))))
-(check-sat)
-(exit)
diff --git a/tests/smtlib2/uf/unsat/eq_diamond2.smt2 b/tests/smtlib2/uf/unsat/eq_diamond2.smt2
deleted file mode 100644
index e5fd59452..000000000
--- a/tests/smtlib2/uf/unsat/eq_diamond2.smt2
+++ /dev/null
@@ -1,20 +0,0 @@
-(set-logic QF_UF)
-(set-info :source |
-Generating minimum transitivity constraints in P-time for deciding Equality Logic,
-Ofer Strichman and Mirron Rozanov,
-SMT Workshop 2005.
-
-Translator: Leonardo de Moura. |)
-(set-info :smt-lib-version 2.0)
-(set-info :category "crafted")
-(set-info :status unsat)
-(declare-sort U 0)
-(declare-fun x0 () U)
-(declare-fun y0 () U)
-(declare-fun z0 () U)
-(declare-fun x1 () U)
-(declare-fun y1 () U)
-(declare-fun z1 () U)
-(assert (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) (not (= x0 x1))))
-(check-sat)
-(exit)
diff --git a/tests/smtlib2/uf/unsat/equality_norm_set.smt2 b/tests/smtlib2/uf/unsat/equality_norm_set.smt2
deleted file mode 100644
index c5e38a47e..000000000
--- a/tests/smtlib2/uf/unsat/equality_norm_set.smt2
+++ /dev/null
@@ -1,12 +0,0 @@
-(set-logic QF_UF)
-(declare-sort S1 0)
-(declare-sort S0 0)
-(declare-fun v0 () S0)
-(assert
- (let ((?n1 true))
- (let ((?n2 (ite ?n1 v0 v0)))
- (let ((?n3 (= v0 ?n2)))
- (let ((?n4 (xor ?n1 ?n3))) ?n4
-)))))
-(check-sat)
-(exit)
diff --git a/tests/smtlib2/uf/unsat/xor.smt2 b/tests/smtlib2/uf/unsat/xor.smt2
deleted file mode 100644
index 916b434f5..000000000
--- a/tests/smtlib2/uf/unsat/xor.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-(set-logic QF_UF)
-(declare-fun _substvar_1662_ () Bool)
-(declare-fun _substvar_2244_ () Bool)
-(assert
- (let ((e183 (xor _substvar_2244_ _substvar_2244_)))
- (let ((e184 (not e183)))
- (let ((e185 (= _substvar_1662_ _substvar_1662_)))
- (let ((e186 (xor e184 e185)))
- e186)))))
-(check-sat)
-
--
GitLab