diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index 3f573aa7fb..e04b783523 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -59,7 +59,7 @@ This should be the case Tableaux solver as well: (error "Model generation disabled (try --produce-models)") The messages above mention `--produce-models`, but we can also use -`set-option`. This requires the Tableaux solver, however: +`set-option`. $ echo '(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2 (error "No model produced.") @@ -67,12 +67,7 @@ The messages above mention `--produce-models`, but we can also use $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 (error "No model produced.") - $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2 - (error "Model generation requires the Tableaux solver (try --produce-models)") - (error "Model generation disabled (try --produce-models)") - -And now some cases where it should work (using either `--produce-models` or -`Tableaux` with `set-option`): +And now some cases where it should work (using either `--produce-models` or `set-option`): $ echo '(check-sat)(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2 2>/dev/null @@ -80,6 +75,11 @@ And now some cases where it should work (using either `--produce-models` or ( ) + $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2 2>/dev/null + + unknown + ( + ) $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 2>/dev/null unknown diff --git a/tests/dune.inc b/tests/dune.inc index e6a429ad8c..3d4a7d522b 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -175627,8 +175627,8 @@ ; Auto-generated part begin (subdir issues (rule - (target 777.models.fail_tableaux.output) - (deps (:input 777.models.fail.smt2)) + (target 777.models_tableaux.output) + (deps (:input 777.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -175643,11 +175643,11 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps 777.models.fail_tableaux.output) + (deps 777.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (ignore-stdout (with-accepted-exit-codes (not 0) (run diff 777.models.fail.expected 777.models.fail_tableaux.output))))) + (diff 777.models.expected 777.models_tableaux.output))) (rule (target 696_ci_cdcl_no_minimal_bj.output) (deps (:input 696.ae)) @@ -176459,8 +176459,8 @@ (action (diff 645.expected 645_fpa.output))) (rule - (target 555.models.fail_tableaux.output) - (deps (:input 555.models.fail.smt2)) + (target 555.models_tableaux.output) + (deps (:input 555.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176475,11 +176475,11 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps 555.models.fail_tableaux.output) + (deps 555.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (ignore-stdout (with-accepted-exit-codes (not 0) (run diff 555.models.fail.expected 555.models.fail_tableaux.output))))) + (diff 555.models.expected 555.models_tableaux.output))) (rule (target 479_ci_cdcl_no_minimal_bj.output) (deps (:input 479.smt2)) @@ -192240,8 +192240,8 @@ ; Auto-generated part begin (subdir models/arith (rule - (target arith2.models.fail_tableaux.output) - (deps (:input arith2.models.fail.smt2)) + (target arith2.models_tableaux.output) + (deps (:input arith2.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192256,14 +192256,14 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps arith2.models.fail_tableaux.output) + (deps arith2.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (ignore-stdout (with-accepted-exit-codes (not 0) (run diff arith2.models.fail.expected arith2.models.fail_tableaux.output))))) + (diff arith2.models.expected arith2.models_tableaux.output))) (rule - (target arith1.models.fail_tableaux.output) - (deps (:input arith1.models.fail.smt2)) + (target arith1.models_tableaux.output) + (deps (:input arith1.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192278,19 +192278,19 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps arith1.models.fail_tableaux.output) + (deps arith1.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (ignore-stdout (with-accepted-exit-codes (not 0) (run diff arith1.models.fail.expected arith1.models.fail_tableaux.output)))))) + (diff arith1.models.expected arith1.models_tableaux.output)))) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/bool (rule - (target bool2.models.fail_tableaux.output) - (deps (:input bool2.models.fail.smt2)) + (target bool2.models_tableaux.output) + (deps (:input bool2.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192305,14 +192305,14 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps bool2.models.fail_tableaux.output) + (deps bool2.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (ignore-stdout (with-accepted-exit-codes (not 0) (run diff bool2.models.fail.expected bool2.models.fail_tableaux.output))))) + (diff bool2.models.expected bool2.models_tableaux.output))) (rule - (target bool1.models.fail_tableaux.output) - (deps (:input bool1.models.fail.smt2)) + (target bool1.models_tableaux.output) + (deps (:input bool1.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192327,11 +192327,11 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps bool1.models.fail_tableaux.output) + (deps bool1.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (ignore-stdout (with-accepted-exit-codes (not 0) (run diff bool1.models.fail.expected bool1.models.fail_tableaux.output)))))) + (diff bool1.models.expected bool1.models_tableaux.output)))) ; Auto-generated part end ; File auto-generated by gentests @@ -192365,8 +192365,8 @@ ; Auto-generated part begin (subdir models/issues/715 (rule - (target 715_2.models.fail_tableaux.output) - (deps (:input 715_2.models.fail.smt2)) + (target 715_2.models_tableaux.output) + (deps (:input 715_2.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192381,11 +192381,11 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps 715_2.models.fail_tableaux.output) + (deps 715_2.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (ignore-stdout (with-accepted-exit-codes (not 0) (run diff 715_2.models.fail.expected 715_2.models.fail_tableaux.output))))) + (diff 715_2.models.expected 715_2.models_tableaux.output))) (rule (target 715_1.models_tableaux.output) (deps (:input 715_1.models.ae)) @@ -192414,8 +192414,8 @@ ; Auto-generated part begin (subdir models/records (rule - (target record1.models.fail_tableaux.output) - (deps (:input record1.models.fail.smt2)) + (target record1.models_tableaux.output) + (deps (:input record1.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192430,19 +192430,19 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps record1.models.fail_tableaux.output) + (deps record1.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (ignore-stdout (with-accepted-exit-codes (not 0) (run diff record1.models.fail.expected record1.models.fail_tableaux.output)))))) + (diff record1.models.expected record1.models_tableaux.output)))) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/uf (rule - (target uf2.models.fail_tableaux.output) - (deps (:input uf2.models.fail.smt2)) + (target uf2.models_tableaux.output) + (deps (:input uf2.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192457,14 +192457,14 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps uf2.models.fail_tableaux.output) + (deps uf2.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (ignore-stdout (with-accepted-exit-codes (not 0) (run diff uf2.models.fail.expected uf2.models.fail_tableaux.output))))) + (diff uf2.models.expected uf2.models_tableaux.output))) (rule - (target uf1.models.fail_tableaux.output) - (deps (:input uf1.models.fail.smt2)) + (target uf1.models_tableaux.output) + (deps (:input uf1.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192479,11 +192479,11 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps uf1.models.fail_tableaux.output) + (deps uf1.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (ignore-stdout (with-accepted-exit-codes (not 0) (run diff uf1.models.fail.expected uf1.models.fail_tableaux.output)))))) + (diff uf1.models.expected uf1.models_tableaux.output)))) ; Auto-generated part end ; File auto-generated by gentests