1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[FAIL] (set-option :there-is-no-such-option bad argument)
*** Data.SBV: Unexpected non-success response from Z3:
***
*** Sent : (set-option :there-is-no-such-option bad argument)
*** Expected : success
*** Received : (error "line 5 column 37: unknown parameter 'there_is_no_such_option'
*** Legal parameters are:
*** auto_config (bool) (default: true)
*** debug_ref_count (bool) (default: false)
*** dot_proof_file (string) (default: proof.dot)
*** dump_models (bool) (default: false)
*** memory_high_watermark (unsigned int) (default: 0)
*** memory_max_alloc_count (unsigned int) (default: 0)
*** memory_max_size (unsigned int) (default: 0)
*** model (bool) (default: true)
*** model_compress (bool) (default: true)
*** model_validate (bool) (default: false)
*** proof (bool) (default: false)
*** rlimit (unsigned int) (default: 0)
*** smtlib2_compliant (bool) (default: false)
*** stats (bool) (default: false)
*** timeout (unsigned int) (default: 4294967295)
*** trace (bool) (default: false)
*** trace_file_name (string) (default: z3.log)
*** type_check (bool) (default: true)
*** unsat_core (bool) (default: false)
*** verbose (unsigned int) (default: 0)
*** warning (bool) (default: true)
*** well_sorted_check (bool) (default: false)")
***
*** Exit code : ExitFailure (-15)
*** Executable: /usr/local/bin/z3
*** Options : -nw -in -smt2
***
*** Reason : Backend solver reports it does not support this option.
*** Check the spelling, and if correct please report this as a
*** bug/feature request with the solver!
|
