qOpt_1.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")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () Int 1)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () Int) ; tracks user variable "x1"
[GOOD] (declare-fun s4 () Int) ; tracks user variable "x2"
[GOOD] (declare-fun s7 () Int) ; tracks user variable "x3"
[GOOD] (declare-fun s10 () Int) ; tracks user variable "x4"
[GOOD] (declare-fun s13 () Int) ; tracks user variable "x5"
[GOOD] ; --- optimization tracker variables ---
[GOOD] (declare-fun s3 () Int) ; tracks goal1
[GOOD] (declare-fun s6 () Int) ; tracks goal2
[GOOD] (declare-fun s9 () Int) ; tracks goal3
[GOOD] (declare-fun s12 () Int) ; tracks goal4
[GOOD] (declare-fun s15 () Int) ; tracks goal5
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s2 () Bool (<= s1 s0))
[GOOD] (define-fun s5 () Bool (<= s1 s4))
[GOOD] (define-fun s8 () Bool (<= s1 s7))
[GOOD] (define-fun s11 () Bool (<= s1 s10))
[GOOD] (define-fun s14 () Bool (<= s1 s13))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s2)
[GOOD] (assert s5)
[GOOD] (assert s8)
[GOOD] (assert s11)
[GOOD] (assert s14)
[GOOD] (assert (= s0 s3))
[GOOD] (maximize s3)
[GOOD] (assert (= s4 s6))
[GOOD] (maximize s6)
[GOOD] (assert (= s7 s9))
[GOOD] (maximize s9)
[GOOD] (assert (= s10 s12))
[GOOD] (maximize s12)
[GOOD] (assert (= s13 s15))
[GOOD] (maximize s15)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-objectives)
[RECV] (objectives
        (s3 oo)
        (s6  (interval (* (- 1) oo) oo))
        (s9  (interval (* (- 1) oo) oo))
        (s12  (interval (* (- 1) oo) oo))
        (s15  (interval (* (- 1) oo) oo))
       )
[SEND] (get-value (s0))
[RECV] ((s0 1))
[SEND] (get-value (s4))
[RECV] ((s4 1))
[SEND] (get-value (s7))
[RECV] ((s7 1))
[SEND] (get-value (s10))
[RECV] ((s10 1))
[SEND] (get-value (s13))
[RECV] ((s13 1))
[SEND] (get-value (s3))
[RECV] ((s3 1))
[SEND] (get-value (s6))
[RECV] ((s6 1))
[SEND] (get-value (s9))
[RECV] ((s9 1))
[SEND] (get-value (s12))
[RECV] ((s12 1))
[SEND] (get-value (s15))
[RECV] ((s15 1))
[SEND] (get-objectives)
[RECV] (objectives
        (s3 oo)
        (s6  (interval (* (- 1) oo) oo))
        (s9  (interval (* (- 1) oo) oo))
        (s12  (interval (* (- 1) oo) oo))
        (s15  (interval (* (- 1) oo) oo))
       )
*** Solver   : Z3
*** Exit code: ExitFailure (-15)

EXCEPTION CAUGHT:

*** Data.SBV.getValue: The current solver state is satisfiable in an extension field.
*** That is, the optimized values assume epsilon/infinity values.
***
*** Calls to getValue is not supported in this context. Instead, use the 'optimize' method
*** directly and inspect the objective values explicitly.
***
*** The current model is:
***
***     Optimal in an extension field:
***       goal1 =          oo :: Integer
***       goal2 = [-oo .. oo] :: [Integer]
***       goal3 = [-oo .. oo] :: [Integer]
***       goal4 = [-oo .. oo] :: [Integer]
***       goal5 = [-oo .. oo] :: [Integer]