query_badOption.gold

** 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)
***                  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_validate (bool) (default: false)
***                  proof (bool) (default: false)
***                  rlimit (unsigned int) (default: 0)
***                  smtlib2_compliant (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
***
*** 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!

CallStack (from HasCallStack):
  error, called at ./Data/SBV/SMT/SMT.hs:722:61 in sbv-7.2-BmAQsjRcnLN24H2yOFpcOt:Data.SBV.SMT.SMT