diff --git a/tests/dune.inc b/tests/dune.inc index ca1d264a2..62c2b6d2f 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -175989,7 +175989,7 @@ (action (diff test_float3.fpa.expected test_float3.fpa_fpa.output))) (rule - (target test_float2.models_tableaux.output) + (target test_float2.models_dolmen.output) (deps (:input test_float2.models.smt2)) (package alt-ergo) (action @@ -176002,14 +176002,13 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps test_float2.models_tableaux.output) + (deps test_float2.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff test_float2.models.expected test_float2.models_tableaux.output))) + (diff test_float2.models.expected test_float2.models_dolmen.output))) (rule (target test_float1.dolmen_dolmen.output) (deps (:input test_float1.dolmen.smt2)) @@ -176037,7 +176036,7 @@ ; Auto-generated part begin (subdir issues (rule - (target 926.models_tableaux.output) + (target 926.models_dolmen.output) (deps (:input 926.models.smt2)) (package alt-ergo) (action @@ -176050,14 +176049,13 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps 926.models_tableaux.output) + (deps 926.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff 926.models.expected 926.models_tableaux.output))) + (diff 926.models.expected 926.models_dolmen.output))) (rule (target 889_ci_cdcl_no_minimal_bj.output) (deps (:input 889.smt2)) @@ -176329,7 +176327,7 @@ (action (diff 883.dolmen.expected 883.dolmen_dolmen.output))) (rule - (target 777.models_tableaux.output) + (target 777.models_dolmen.output) (deps (:input 777.models.smt2)) (package alt-ergo) (action @@ -176342,14 +176340,13 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps 777.models_tableaux.output) + (deps 777.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff 777.models.expected 777.models_tableaux.output))) + (diff 777.models.expected 777.models_dolmen.output))) (rule (target 696_ci_cdcl_no_minimal_bj.output) (deps (:input 696.ae)) @@ -177140,7 +177137,7 @@ (action (diff 645.expected 645_fpa.output))) (rule - (target 555.models_tableaux.output) + (target 555.models_dolmen.output) (deps (:input 555.models.smt2)) (package alt-ergo) (action @@ -177153,14 +177150,13 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps 555.models_tableaux.output) + (deps 555.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff 555.models.expected 555.models_tableaux.output))) + (diff 555.models.expected 555.models_dolmen.output))) (rule (target 479_ci_cdcl_no_minimal_bj.output) (deps (:input 479.smt2)) @@ -178797,7 +178793,7 @@ ; Auto-generated part begin (subdir issues/854 (rule - (target twice_eq.models_tableaux.output) + (target twice_eq.models_dolmen.output) (deps (:input twice_eq.models.smt2)) (package alt-ergo) (action @@ -178810,16 +178806,15 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps twice_eq.models_tableaux.output) + (deps twice_eq.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff twice_eq.models.expected twice_eq.models_tableaux.output))) + (diff twice_eq.models.expected twice_eq.models_dolmen.output))) (rule - (target original.models_tableaux.output) + (target original.models_dolmen.output) (deps (:input original.models.smt2)) (package alt-ergo) (action @@ -178832,16 +178827,15 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps original.models_tableaux.output) + (deps original.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff original.models.expected original.models_tableaux.output))) + (diff original.models.expected original.models_dolmen.output))) (rule - (target function.models_tableaux.output) + (target function.models_dolmen.output) (deps (:input function.models.smt2)) (package alt-ergo) (action @@ -178854,14 +178848,13 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps function.models_tableaux.output) + (deps function.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff function.models.expected function.models_tableaux.output)))) + (diff function.models.expected function.models_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests @@ -192902,7 +192895,7 @@ ; Auto-generated part begin (subdir models (rule - (target check_sat.models_tableaux.output) + (target check_sat.models_dolmen.output) (deps (:input check_sat.models.ae)) (package alt-ergo) (action @@ -192915,14 +192908,13 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps check_sat.models_tableaux.output) + (deps check_sat.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff check_sat.models.expected check_sat.models_tableaux.output)))) + (diff check_sat.models.expected check_sat.models_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests @@ -193090,7 +193082,7 @@ (action (diff arith3.optimize.expected arith3.optimize_optimize.output))) (rule - (target arith2.models_tableaux.output) + (target arith2.models_dolmen.output) (deps (:input arith2.models.smt2)) (package alt-ergo) (action @@ -193103,14 +193095,13 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps arith2.models_tableaux.output) + (deps arith2.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff arith2.models.expected arith2.models_tableaux.output))) + (diff arith2.models.expected arith2.models_dolmen.output))) (rule (target arith11.optimize_optimize.output) (deps (:input arith11.optimize.smt2)) @@ -193158,7 +193149,7 @@ (action (diff arith10.optimize.expected arith10.optimize_optimize.output))) (rule - (target arith1.models_tableaux.output) + (target arith1.models_dolmen.output) (deps (:input arith1.models.smt2)) (package alt-ergo) (action @@ -193171,21 +193162,20 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps arith1.models_tableaux.output) + (deps arith1.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff arith1.models.expected arith1.models_tableaux.output)))) + (diff arith1.models.expected arith1.models_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/array (rule - (target array1.models_tableaux.output) + (target array1.models_dolmen.output) (deps (:input array1.models.smt2)) (package alt-ergo) (action @@ -193198,21 +193188,20 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps array1.models_tableaux.output) + (deps array1.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff array1.models.expected array1.models_tableaux.output)))) + (diff array1.models.expected array1.models_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/bitv (rule - (target specified.models_tableaux.output) + (target specified.models_dolmen.output) (deps (:input specified.models.smt2)) (package alt-ergo) (action @@ -193225,16 +193214,15 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps specified.models_tableaux.output) + (deps specified.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff specified.models.expected specified.models_tableaux.output))) + (diff specified.models.expected specified.models_dolmen.output))) (rule - (target not.models_tableaux.output) + (target not.models_dolmen.output) (deps (:input not.models.smt2)) (package alt-ergo) (action @@ -193247,16 +193235,15 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps not.models_tableaux.output) + (deps not.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff not.models.expected not.models_tableaux.output))) + (diff not.models.expected not.models_dolmen.output))) (rule - (target extract.models_tableaux.output) + (target extract.models_dolmen.output) (deps (:input extract.models.smt2)) (package alt-ergo) (action @@ -193269,16 +193256,15 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps extract.models_tableaux.output) + (deps extract.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff extract.models.expected extract.models_tableaux.output))) + (diff extract.models.expected extract.models_dolmen.output))) (rule - (target cardinal.models_tableaux.output) + (target cardinal.models_dolmen.output) (deps (:input cardinal.models.smt2)) (package alt-ergo) (action @@ -193291,21 +193277,20 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps cardinal.models_tableaux.output) + (deps cardinal.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff cardinal.models.expected cardinal.models_tableaux.output)))) + (diff cardinal.models.expected cardinal.models_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/bool (rule - (target bool3.models_tableaux.output) + (target bool3.models_dolmen.output) (deps (:input bool3.models.smt2)) (package alt-ergo) (action @@ -193318,16 +193303,15 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps bool3.models_tableaux.output) + (deps bool3.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff bool3.models.expected bool3.models_tableaux.output))) + (diff bool3.models.expected bool3.models_dolmen.output))) (rule - (target bool2.models_tableaux.output) + (target bool2.models_dolmen.output) (deps (:input bool2.models.smt2)) (package alt-ergo) (action @@ -193340,16 +193324,15 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps bool2.models_tableaux.output) + (deps bool2.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff bool2.models.expected bool2.models_tableaux.output))) + (diff bool2.models.expected bool2.models_dolmen.output))) (rule - (target bool1.models_tableaux.output) + (target bool1.models_dolmen.output) (deps (:input bool1.models.smt2)) (package alt-ergo) (action @@ -193362,21 +193345,20 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps bool1.models_tableaux.output) + (deps bool1.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff bool1.models.expected bool1.models_tableaux.output)))) + (diff bool1.models.expected bool1.models_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/issues (rule - (target 719.models.err_tableaux.output) + (target 719.models.err_dolmen.output) (deps (:input 719.models.err.smt2)) (package alt-ergo) (action @@ -193389,21 +193371,20 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps 719.models.err_tableaux.output) + (deps 719.models.err_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff 719.models.err.expected 719.models.err_tableaux.output)))) + (diff 719.models.err.expected 719.models.err_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/issues/715 (rule - (target 715_2.models_tableaux.output) + (target 715_2.models_dolmen.output) (deps (:input 715_2.models.smt2)) (package alt-ergo) (action @@ -193416,16 +193397,15 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps 715_2.models_tableaux.output) + (deps 715_2.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff 715_2.models.expected 715_2.models_tableaux.output))) + (diff 715_2.models.expected 715_2.models_dolmen.output))) (rule - (target 715_1.models_tableaux.output) + (target 715_1.models_dolmen.output) (deps (:input 715_1.models.ae)) (package alt-ergo) (action @@ -193438,21 +193418,20 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps 715_1.models_tableaux.output) + (deps 715_1.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff 715_1.models.expected 715_1.models_tableaux.output)))) + (diff 715_1.models.expected 715_1.models_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/records (rule - (target record1.models_tableaux.output) + (target record1.models_dolmen.output) (deps (:input record1.models.smt2)) (package alt-ergo) (action @@ -193465,21 +193444,20 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps record1.models_tableaux.output) + (deps record1.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff record1.models.expected record1.models_tableaux.output)))) + (diff record1.models.expected record1.models_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/uf (rule - (target uf2.models_tableaux.output) + (target uf2.models_dolmen.output) (deps (:input uf2.models.smt2)) (package alt-ergo) (action @@ -193492,16 +193470,15 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps uf2.models_tableaux.output) + (deps uf2.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff uf2.models.expected uf2.models_tableaux.output))) + (diff uf2.models.expected uf2.models_dolmen.output))) (rule - (target uf1.models_tableaux.output) + (target uf1.models_dolmen.output) (deps (:input uf1.models.smt2)) (package alt-ergo) (action @@ -193514,14 +193491,13 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps uf1.models_tableaux.output) + (deps uf1.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff uf1.models.expected uf1.models_tableaux.output)))) + (diff uf1.models.expected uf1.models_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests diff --git a/tests/models/bool/bool1.models.expected b/tests/models/bool/bool1.models.expected index 8aafa780c..c0aea9281 100644 --- a/tests/models/bool/bool1.models.expected +++ b/tests/models/bool/bool1.models.expected @@ -4,7 +4,7 @@ unknown (define-fun q () Bool false) ) ((notp unknown) - (notnq true)) + (notnq unknown)) unknown @@ -12,6 +12,6 @@ unknown (define-fun p () Bool true) (define-fun q () Bool true) ) -((notp false) - (notnq false)) +((notp unknown) + (notnq unknown)) diff --git a/tests/models/bool/bool3.models.expected b/tests/models/bool/bool3.models.expected index bd76cec77..3ef7afec3 100644 --- a/tests/models/bool/bool3.models.expected +++ b/tests/models/bool/bool3.models.expected @@ -1,9 +1,9 @@ unknown ( - (define-fun x () Bool true) - (define-fun y () Bool true) + (define-fun x () Bool false) + (define-fun y () Bool false) ) -((foo true) +((foo unknown) (bar unknown)) diff --git a/tools/gentest.ml b/tools/gentest.ml index 4966f5ac7..0a86c7637 100644 --- a/tools/gentest.ml +++ b/tools/gentest.ml @@ -258,7 +258,7 @@ end = struct acc with exclude = "legacy" :: "fpa" :: acc.exclude; - filters = Some ["tableaux"] + filters = Some ["dolmen"] } | "fpa" -> {acc with filters = Some ["fpa"]}