Skip to content
Snippets Groups Projects
Normal view Permalink
dune.inc 10 KiB
Newer Older
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
1 
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
2 
--dont-print-result %{dep:bag-BagImpl-createqtvc.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
3 4 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:bag-BagImpl-createqtvc.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
5 
--dont-print-result %{dep:div_abs.smt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
6 7 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_abs.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
8 
--dont-print-result %{dep:fact-FactRecursive-fact_recqtvc.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
9 10 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:fact-FactRecursive-fact_recqtvc.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
[Trigger] remove variable as possible triggers  
François Bobot committed
11 
--dont-print-result %{dep:float_interval-GenericFloat-add_special_1.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
12 13 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:float_interval-GenericFloat-add_special_1.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
14 
--dont-print-result %{dep:interval-Convexe-exists_memqtvc_1.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
15 16 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:interval-Convexe-exists_memqtvc_1.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
17 
--dont-print-result %{dep:interval-Convexe-exists_memqtvc_2.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
18 19 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:interval-Convexe-exists_memqtvc_2.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
20 
--dont-print-result %{dep:lost_in_search_union.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
21 22 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:lost_in_search_union.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
[Definition] add limited eager folding  
François Bobot committed
23 24 25 
--dont-print-result %{dep:mjrty-Mjrty-mjrtyqtvc_3.psmt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mjrty-Mjrty-mjrtyqtvc_3.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
26 
--dont-print-result %{dep:mul_abs.smt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
27 28 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_abs.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
29 
--dont-print-result %{dep:ordered_is_ordered.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
30 31 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:ordered_is_ordered.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Add definition folding  
François Bobot committed
32 
--dont-print-result %{dep:range_loop_invariant_CHECK_preserved_Why3_Colibri2_n_a.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
33 34 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:range_loop_invariant_CHECK_preserved_Why3_Colibri2_n_a.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Add definition folding  
François Bobot committed
35 
--dont-print-result %{dep:range_loop_invariant_CHECK_preserved_Why3_Colibri2_n_a_simplified.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
36 37 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:range_loop_invariant_CHECK_preserved_Why3_Colibri2_n_a_simplified.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
38 
--dont-print-result %{dep:union-Union-interqtvc_10.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
39 40 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-interqtvc_10.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
41 
--dont-print-result %{dep:union-Union-interqtvc_5.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
42 43 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-interqtvc_5.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
44 
--dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
45 46 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
47 
--dont-print-result %{dep:union-Union-is_singletonqtvc_2.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
48 49 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_2.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
50 
--dont-print-result %{dep:union-Union-is_singletonqtvc_5.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
51 52 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_5.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
53 
--dont-print-result %{dep:union-Union-length0_positiveqtvc_1.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
54 55 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-length0_positiveqtvc_1.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
56 
--dont-print-result %{dep:work_with_fourier_not_simplex.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
57 58 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:work_with_fourier_not_simplex.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
Attach each test to its package  
François Bobot committed
59 
--dont-print-result %{dep:work_with_fourier_not_simplex2.psmt2})) (package colibri2))
François Bobot's avatar
Deactivate by default print-success  
François Bobot committed
60 
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:work_with_fourier_not_simplex2.psmt2})) (package colibri2))
François Bobot's avatar
[Tests] Tests for ceil and floor  
François Bobot committed
61 62 63 
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
--dont-print-result %{dep:wp_initialize.psmt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_initialize.psmt2})) (package colibri2))
François Bobot's avatar
[Quantifier] Fix delayed instantiation for false existential  
François Bobot committed
64 
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
[Choice] Fix successive add_to_group and simplify  
François Bobot committed
65 66 67 
--dont-print-result %{dep:wp_sharing_f_ensures.psmt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_sharing_f_ensures.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
[Quantifier] Register the delayed substitution attached to quantifiers  
François Bobot committed
68 69 70 
--dont-print-result %{dep:wp_simpl_is_type_f_ensures.psmt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_simpl_is_type_f_ensures.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
François Bobot's avatar
[Quantifier] Fix delayed instantiation for false existential  
François Bobot committed
71 72 
--dont-print-result %{dep:wp_simpl_is_type_g_ensures.psmt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_simpl_is_type_g_ensures.psmt2})) (package colibri2))
François Bobot's avatar
[Quant] Fix instantiantiation vs decision  
François Bobot committed
73 74 75 
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
--dont-print-result %{dep:wp_terminates_formulae_decreases_variant.psmt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_terminates_formulae_decreases_variant.psmt2})) (package colibri2))