** 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] (define-fun s3 () Int 10)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () Int) ; tracks user variable "x1"
[GOOD] (declare-fun s6 () Int) ; tracks user variable "x2"
[GOOD] (declare-fun s10 () Int) ; tracks user variable "x3"
[GOOD] (declare-fun s14 () Int) ; tracks user variable "x4"
[GOOD] (declare-fun s18 () Int) ; tracks user variable "x5"
[GOOD] ; --- optimization tracker variables ---
[GOOD] (declare-fun s5 () Int) ; tracks goal1
[GOOD] (declare-fun s9 () Int) ; tracks goal2
[GOOD] (declare-fun s13 () Int) ; tracks goal3
[GOOD] (declare-fun s17 () Int) ; tracks goal4
[GOOD] (declare-fun s21 () 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 s4 () Bool (< s0 s3))
[GOOD] (define-fun s7 () Bool (<= s1 s6))
[GOOD] (define-fun s8 () Bool (< s6 s3))
[GOOD] (define-fun s11 () Bool (<= s1 s10))
[GOOD] (define-fun s12 () Bool (< s10 s3))
[GOOD] (define-fun s15 () Bool (<= s1 s14))
[GOOD] (define-fun s16 () Bool (< s14 s3))
[GOOD] (define-fun s19 () Bool (<= s1 s18))
[GOOD] (define-fun s20 () Bool (< s18 s3))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s2)
[GOOD] (assert s4)
[GOOD] (assert s7)
[GOOD] (assert s8)
[GOOD] (assert s11)
[GOOD] (assert s12)
[GOOD] (assert s15)
[GOOD] (assert s16)
[GOOD] (assert s19)
[GOOD] (assert s20)
[GOOD] (assert (= s0 s5))
[GOOD] (maximize s5)
[GOOD] (assert (= s6 s9))
[GOOD] (maximize s9)
[GOOD] (assert (= s10 s13))
[GOOD] (maximize s13)
[GOOD] (assert (= s14 s17))
[GOOD] (maximize s17)
[GOOD] (assert (= s18 s21))
[GOOD] (maximize s21)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-objectives)
[RECV] (objectives
        (s5 9)
        (s9 9)
        (s13 9)
        (s17 9)
        (s21 9)
       )
[SEND] (get-value (s0))
[RECV] ((s0 9))
[SEND] (get-objectives)
[RECV] (objectives
        (s5 9)
        (s9 9)
        (s13 9)
        (s17 9)
        (s21 9)
       )
[SEND] (get-value (s6))
[RECV] ((s6 9))
[SEND] (get-objectives)
[RECV] (objectives
        (s5 9)
        (s9 9)
        (s13 9)
        (s17 9)
        (s21 9)
       )
[SEND] (get-value (s10))
[RECV] ((s10 9))
[SEND] (get-objectives)
[RECV] (objectives
        (s5 9)
        (s9 9)
        (s13 9)
        (s17 9)
        (s21 9)
       )
[SEND] (get-value (s14))
[RECV] ((s14 9))
[SEND] (get-objectives)
[RECV] (objectives
        (s5 9)
        (s9 9)
        (s13 9)
        (s17 9)
        (s21 9)
       )
[SEND] (get-value (s18))
[RECV] ((s18 9))
*** Solver   : Z3
*** Exit code: ExitSuccess

 FINAL:[9,9,9,9,9]
DONE!