Rec-Fun and QBVF

[mrkmarron]

I am seeing unusual behavior with the solver quickly returning unknown instead of unsat when a formula has an existential quantifier and a rec-fun.

(define-fun _@@desop_List_Int__hasPredCheck_using_pred--list.bsq_k1..238@7435 ((l List_Int_) (count BNat)) $Result_Bool
($Result_Bool@success (exists ((_@n BNat)) (= _@n BNat@zero))) ;; <---- results in a quick unknown
;; ($Result_Bool@success true)  <---- results in unsat 
)

There is a rec-fun in the repro file. It is actually not doing any recursion and if the formula is constructed without the rec-fun that calls into this quantifier Z3 quickly solves with unsat as well. Full file below:

;;-------------------------------------------------------------------------------------------------------
;; Copyright (C) Microsoft. All rights reserved.
;; Licensed under the MIT license. See LICENSE.txt file in the project root for full license information.
;;-------------------------------------------------------------------------------------------------------

(set-logic ALL)

;;
;; Type Tags
;;

(declare-datatypes (
      (TypeTag 0)
    ) (
    ( 
      (TypeTag_$Invalid)
      (ListOps)
      (TypeTag_BigInt)
      (TypeTag_BigNat)
      (TypeTag_Bool)
      (TypeTag_BufferCompression)
      (TypeTag_BufferFormat)
      (TypeTag_ByteBuffer)
      (TypeTag_ContentHash)
      (TypeTag_Decimal)
      (TypeTag_Float)
      (TypeTag_HavocSequence)
      (TypeTag_ISOTime)
      (TypeTag_Int)
      (TypeTag_ListConcatOps)
      (TypeTag_ListFlatOps)
      (TypeTag_List_Int_)
      (TypeTag_LogicalTime)
      (TypeTag_Nat)
      (TypeTag_None)
      (TypeTag_Nothing)
      (TypeTag_Rational)
      (TypeTag_Regex)
      (TypeTag_String)
      (TypeTag_StringPos)
      (TypeTag_UUID)
    )
))

(declare-datatypes (
      (AbstractTypeTag 0)
    ) (
    ( 
      (AbstractTypeTag_$Invalid)
      ;;NO DATA;;
    )
))

(declare-datatypes (
      (TupleIndexTag 0)
    ) (
    ( 
      (TupleIndexTag_$Invalid)
      ;;NO DATA;;
    )
))

(declare-datatypes (
      (RecordPropertyTag 0)
    ) (
    ( 
      (RecordPropertyTag_$Invalid)
      ;;RecordPropertyTag;;
    )
))

(declare-fun SubtypeOf@ (TypeTag AbstractTypeTag) Bool)
;;NO DATA;;

(declare-fun HasIndex@ (TypeTag TupleIndexTag) Bool)
;;NO DATA;;

(declare-fun HasProperty@ (TypeTag RecordPropertyTag) Bool)
;;NO DATA;;

(declare-fun TypeTagRank@ (TypeTag) Int)
(assert (= (TypeTagRank@ TypeTag_BigInt) 0))
(assert (= (TypeTagRank@ TypeTag_BigNat) 1))
(assert (= (TypeTagRank@ TypeTag_Bool) 2))
(assert (= (TypeTagRank@ TypeTag_BufferCompression) 3))
(assert (= (TypeTagRank@ TypeTag_BufferFormat) 4))
(assert (= (TypeTagRank@ TypeTag_ContentHash) 5))
(assert (= (TypeTagRank@ TypeTag_ISOTime) 6))
(assert (= (TypeTagRank@ TypeTag_Int) 7))
(assert (= (TypeTagRank@ TypeTag_LogicalTime) 8))
(assert (= (TypeTagRank@ TypeTag_Nat) 9))
(assert (= (TypeTagRank@ TypeTag_None) 10))
(assert (= (TypeTagRank@ TypeTag_String) 11))
(assert (= (TypeTagRank@ TypeTag_UUID) 12))

(define-sort BInt () (_ BitVec 8))
(define-sort BNat () (_ BitVec 8))
(define-sort BBigInt () Int)
(define-sort BBigNat () Int)
(define-sort BFloat () Real)
(define-sort BDecimal () Real)
(define-sort BRational () Real)
(define-sort BStringPos () Int)
(define-sort BString () String)
(define-sort BByteBuffer () (Seq (_ BitVec 8)))
(define-sort BISOTime () Int)
(define-sort BLogicalTime () Int)
(define-sort BUUID () (_ BitVec 12)) ;;TODO we should experiment with this encoding -- int, bv128, constructor?
(define-sort BHash () (_ BitVec 16))

;;TODO BHashable and Hash + HashInvert and axioms

(declare-const BInt@zero BInt) (assert (= BInt@zero (_ bv0 8)))
(declare-const BInt@one BInt) (assert (= BInt@one (_ bv1 8)))
(declare-const BInt@min BInt) (assert (= BInt@min #b10000000))
(declare-const BInt@max BInt) (assert (= BInt@max (_ bv127 8)))
(declare-const BNat@zero BNat) (assert (= BNat@zero (_ bv0 8)))
(declare-const BNat@one BNat) (assert (= BNat@one (_ bv1 8)))
(declare-const BNat@min BNat) (assert (= BNat@min BNat@zero))
(declare-const BNat@max BNat) (assert (= BNat@max (_ bv255 8)))

(define-sort HavocSequence () (Seq BNat))

(declare-sort NumericOps 0)
(declare-sort ListFlatOps 0)
(declare-sort ListConcatOps 0)
(declare-sort ListOps 0)

(declare-const BBigInt@zero BBigInt) (assert (= BBigInt@zero 0))
(declare-const BBigInt@one BBigInt) (assert (= BBigInt@one 1))

(declare-const BBigNat@zero BBigNat) (assert (= BBigNat@zero 0))
(declare-const BBigNat@one BBigNat) (assert (= BBigNat@one 1))

(declare-const BFloat@zero BFloat) (assert (= BFloat@zero 0.0))
(declare-const BFloat@one BFloat) (assert (= BFloat@one 1.0))
(declare-const BFloat@pi BFloat) (assert (= BFloat@pi 3.141592653589793))
(declare-const BFloat@e BFloat) (assert (= BFloat@e 2.718281828459045))

(declare-const BDecimal@zero BDecimal) (assert (= BDecimal@zero 0.0))
(declare-const BDecimal@one BDecimal) (assert (= BDecimal@one 1.0))
(declare-const BDecimal@pi BDecimal) (assert (= BDecimal@pi 3.141592653589793))
(declare-const BDecimal@e BDecimal) (assert (= BDecimal@e 2.718281828459045))

(declare-const BRational@zero BRational) (assert (= BRational@zero 0.0))
(declare-const BRational@one BRational) (assert (= BRational@one 1.0))

(declare-fun BByteBuffer@expandstr ((BByteBuffer)) BString)

;;Define the ISequence datatype and operators
(declare-sort ISequence 0)

(declare-fun ISequence@size (ISequence) BNat)
(declare-fun ISequence@get (ISequence BNat) BNat)

(define-fun ISequence@assertSorted ((s ISequence)) Bool
  (let ((len (ISequence@size s)))
    (forall ((i BNat) (j BNat))
      (=> (and (bvult i j) (bvult j len))
          (bvult (ISequence@get s i) (ISequence@get s j))))
  )
)

(define-fun ISequence@assertValuesRange ((s ISequence) (limit BNat)) Bool
  (let ((len (ISequence@size s)))
    (forall ((i BNat))
      (=> (bvult i len)
          (bvult (ISequence@get s i) limit)))
  )
)

(declare-const ISequence@empty ISequence)
(assert (= (ISequence@size ISequence@empty) BNat@zero))

;;Define the JSequence datatype
(declare-datatype JSequencePair ((JSequencePair@cons (JSequencePair@a BNat) (JSequencePair@b BNat))))
(declare-sort JSequence 0)

(declare-fun JSequence@size (JSequence) BNat)
(declare-fun JSequence@get (JSequence BNat) JSequencePair)

(define-fun JSequence@assertSorted ((s JSequence)) Bool
  (let ((len (JSequence@size s)))
    (forall ((i BNat) (j BNat))
      (=> (and (bvult i j) (bvult j len))
          (or 
            (bvult (JSequencePair@a (JSequence@get s i)) (JSequencePair@a (JSequence@get s j)))
            (and (= (JSequencePair@a (JSequence@get s i)) (JSequencePair@a (JSequence@get s j))) (bvult (JSequencePair@b (JSequence@get s i)) (JSequencePair@b (JSequence@get s j))))
          )
      )
    )
  )
)

(define-fun JSequence@assertValuesRange ((s JSequence) (limita BNat) (limitb BNat)) Bool
  (let ((len (JSequence@size s)))
    (forall ((i BNat))
      (=> (bvult i len)
          (and (bvult (JSequencePair@a (JSequence@get s i)) limita) (bvult (JSequencePair@b (JSequence@get s i)) limitb))))
  )
)

(declare-const JSequence@empty JSequence)
(assert (= (JSequence@size JSequence@empty) BNat@zero))

;;Define the SSequence datatype
(declare-sort SSequence 0)

(declare-fun SSequence@size (SSequence) BNat)
(declare-fun SSequence@get (SSequence BNat) BNat)

(define-fun SSequence@assertValuesRange ((s SSequence) (limit BNat)) Bool
  (let ((len (SSequence@size s)))
    (forall ((i BNat))
      (=> (bvult i len)
          (bvult (SSequence@get s i) limit)))
  )
)

(declare-const SSequence@empty SSequence)
(assert (= (SSequence@size SSequence@empty) BNat@zero))

;;
;; Primitive datatypes 
;;
(declare-datatypes (
      (bsq_none 0)
      (bsq_nothing 0)
      ; Bool -> Bool
      ; Int -> BV
      ; Nat -> BV
      ; BigInt -> Int
      ; BigNat -> Int
      ; Float -> Real 
      ; Decimal -> Real
      ; Rational -> Real
      ; StringPos -> Int
      ; String -> String | (Seq (_ BitVec 64))
      ; ByteBuffer -> (Seq (_ BitVec 8))
      ; ISOTime -> Int
      ; LogicalTime -> Int
      ; UUID -> ?? need to investigate
      ; ContentHash -> (_ BitVec X)
    ) (
      ( (bsq_none@literal) ) 
      ( (bsq_nothing@literal) ) 
))

;;
;; KeyType Concept datatypes
;;
(declare-datatypes (
      ;;NO DATA;;
      (bsq_keyobject 0)
      (BKey 0)
    ) (
    ;;NO DATA;;
    (
      (bsqkey_none@literal)
      (bsqkey_nothing@literal) 
      (bsqkey_bool@box (bsqkey_bool_value Bool))
      (bsqkey_int@box (bsqkey_int_value BInt))
      (bsqkey_nat@box (bsqkey_nat_value BNat))
      (bsqkey_bigint@box (bsqkey_bigint_value BBigInt))
      (bsqkey_bignat@box (bsqkey_bignat_value BBigNat))
      (bsqkey_string@box (bsqkey_string_value BString))
      (bsqkey_logicaltime@box (bsqkey_logicaltime_value BLogicalTime))
      (bsqkey_uuid@box (bsqkey_uuid_value BUUID))
      (bsqkey_contenthash@box (bsqkey_contenthash_value BHash))
      (BigInt@box (bsqkey_BigInt_value BBigInt))
      (BigNat@box (bsqkey_BigNat_value BBigNat))
      (ContentHash@box (bsqkey_ContentHash_value BHash))
      (Int@box (bsqkey_Int_value BInt))
      (LogicalTime@box (bsqkey_LogicalTime_value BLogicalTime))
      (Nat@box (bsqkey_Nat_value BNat))
      (BufferFormat@box (bsqkey_BufferFormat_value BNat))
      (BufferCompression@box (bsqkey_BufferCompression_value BNat))
      (Bool@box (bsqkey_Bool_value Bool))
      (None@box (bsqkey_None_value bsq_none))
      (String@box (bsqkey_String_value BString))
      (UUID@box (bsqkey_UUID_value BUUID))
    )
    ( (BKey@box (BKey_type TypeTag) (BKey_value bsq_keyobject)) )
))

(declare-const BKey@none BKey)
(assert (= BKey@none (BKey@box TypeTag_None bsqkey_none@literal)))

(declare-const BKey@nothing BKey)
(assert (= BKey@nothing (BKey@box TypeTag_Nothing bsqkey_nothing@literal)))

(define-fun bsqkey_none@less ((k1 bsq_keyobject) (k2 bsq_keyobject)) Bool
  false
)

(define-fun bsqkey_nothing@less ((k1 bsq_keyobject) (k2 bsq_keyobject)) Bool
  false
)

(define-fun bsqkey_bool@less ((k1 bsq_keyobject) (k2 bsq_keyobject)) Bool
  (and (not (bsqkey_bool_value k1)) (bsqkey_bool_value k2))
)

(define-fun bsqkey_int@less ((k1 bsq_keyobject) (k2 bsq_keyobject)) Bool
  (bvslt (bsqkey_int_value k1) (bsqkey_int_value k2))
)

(define-fun bsqkey_nat@less ((k1 bsq_keyobject) (k2 bsq_keyobject)) Bool
  (bvult (bsqkey_nat_value k1) (bsqkey_nat_value k2))
)

(define-fun bsqkey_bigint@less ((k1 bsq_keyobject) (k2 bsq_keyobject)) Bool
  (< (bsqkey_bigint_value k1) (bsqkey_bigint_value k2))
)

(define-fun bsqkey_bignat@less ((k1 bsq_keyobject) (k2 bsq_keyobject)) Bool
  (< (bsqkey_bignat_value k1) (bsqkey_bignat_value k2))
)

(define-fun bsqkey_string@less ((k1 bsq_keyobject) (k2 bsq_keyobject)) Bool
  (str.< (bsqkey_string_value k1) (bsqkey_string_value k2))
)

(define-fun bsqkey_logicaltime@less ((k1 bsq_keyobject) (k2 bsq_keyobject)) Bool
  (< (bsqkey_logicaltime_value k1) (bsqkey_logicaltime_value k2))
)

(define-fun bsqkey_uuid@less ((k1 bsq_keyobject) (k2 bsq_keyobject)) Bool
  (bvult (bsqkey_uuid_value k1) (bsqkey_uuid_value k2))
)

(define-fun bsqkey_contenthash@less ((k1 bsq_keyobject) (k2 bsq_keyobject)) Bool
  (bvult (bsqkey_contenthash_value k1) (bsqkey_contenthash_value k2))
)

;;
;; Any Concept datatypes
;;
(declare-datatypes (
    (bsq_regex 0)
    ;;NO DATA;;
    ;;NO DATA;;
    (List_Int_$uli 0)
    (List_Int_ 0)
    (bsq_object 0)
    (BTerm 0)
    ) (
    ( (bsq_regex@cons (bsq_regex_value Int)) )
    ;;NO DATA;;
    ;;NO DATA;;
    ( (_@@cons_List_Int__empty ) (_@@cons_List_Int__slice (_@@cons_List_Int__slice_l List_Int_) (_@@cons_List_Int__slice_start BNat) (_@@cons_List_Int__slice_end BNat)) (_@@cons_List_Int__concat2 (_@@cons_List_Int__concat2_left List_Int_) (_@@cons_List_Int__concat2_right List_Int_)) (_@@cons_List_Int__list_1 (_@@cons_List_Int__list_1__0_ BInt)) (_@@cons_List_Int__list_2 (_@@cons_List_Int__list_2__0_ BInt) (_@@cons_List_Int__list_2__1_ BInt)) (_@@cons_List_Int__list_3 (_@@cons_List_Int__list_3__0_ BInt) (_@@cons_List_Int__list_3__1_ BInt) (_@@cons_List_Int__list_3__2_ BInt)) (_@@cons_List_Int__havoc (_@@cons_List_Int__havoc_path HavocSequence)) )
    ( (List_Int_@cons (List_Int_@size BNat) (List_Int_@uli List_Int_$uli)) )
    (
      (bsqobject_float@box (bsqobject_float_value BFloat))
      (bsqobject_decimal@box (bsqobject_decimal_value BDecimal))
      (bsqobject_rational@box (bsqobject_rational_value BRational))
      (bsqobject_stringpos@box (bsqobject_stringpos_value Int))
      (bsqobject_bytebuffer@box (bsqobject_bytebuffer_value BByteBuffer))
      (bsqobject_isotime@box (bsqobject_isotime_value Int))
      (bsqobject_regex@box (bsqobject_regex_value bsq_regex))
      ;;NO DATA;;
      ;;NO DATA;;
      (ByteBuffer@box (bsqobject_ByteBuffer_value BByteBuffer))
      (Decimal@box (bsqobject_Decimal_value BDecimal))
      (Float@box (bsqobject_Float_value BFloat))
      (ISOTime@box (bsqobject_ISOTime_value BISOTime))
      (Rational@box (bsqobject_Rational_value BRational))
      (Nothing@box (bsqobject_Nothing_value bsq_nothing))
      (Regex@box (bsqobject_Regex_value bsq_regex))
      (StringPos@box (bsqobject_StringPos_value BStringPos))
      (HavocSequence@box (bsqobject_HavocSequence_value HavocSequence))
      (ListConcatOps@box (bsqobject_ListConcatOps_value ListConcatOps))
      (ListFlatOps@box (bsqobject_ListFlatOps_value ListFlatOps))
      (ListOps@box (bsqobject_ListOps_value ListOps))
      (List_Int_@box (bsqobject_List_Int__value List_Int_))
    )
    ( 
      (BTerm@termbox (BTerm_termtype TypeTag) (BTerm_termvalue bsq_object))
      (BTerm@keybox (BTerm_keyvalue BKey)) 
    )
))

(declare-const BTerm@none BTerm)
(assert (= BTerm@none (BTerm@keybox BKey@none)))

(declare-const BTerm@nothing BTerm)
(assert (= BTerm@nothing (BTerm@keybox BKey@nothing)))

(declare-const List_Int_@empty_const List_Int_) (assert (= List_Int_@empty_const (List_Int_@cons BNat@zero _@@cons_List_Int__empty)))

;;
;;Define utility functions
;;
(define-fun GetTypeTag@BKey ((t BKey)) TypeTag
  (BKey_type t)
)

(define-fun GetTypeTag@BTerm ((t BTerm)) TypeTag
  (ite ((_ is BTerm@termbox) t) (BTerm_termtype t) (BKey_type (BTerm_keyvalue t)))
)

;;
;; Ephemeral datatypes
;;
(declare-datatypes (
    (elistnull 0)
    ;;NO DATA;;
    ) (
    ( (elistnull@cons) )
    ;;NO DATA;;
))

(declare-datatypes (
      (ErrorID 0)
    ) (
    ( 
      (ErrorID_AssumeCheck)
      (ErrorID_Target)
    )
))

(declare-datatypes (
      ($Result_BTerm 0)
      ($Result_BBigInt 0)
      ($Result_BBigNat 0)
      ($Result_Bool 0)
      ($Result_BByteBuffer 0)
      ($Result_BHash 0)
      ($Result_BDecimal 0)
      ($Result_BFloat 0)
      ($Result_HavocSequence 0)
      ($Result_BInt 0)
      ($Result_BISOTime 0)
      ($Result_BKey 0)
      ($Result_List_Int_ 0)
      ($Result_ListConcatOps 0)
      ($Result_ListFlatOps 0)
      ($Result_ListOps 0)
      ($Result_BLogicalTime 0)
      ($Result_BNat 0)
      ($Result_bsq_none 0)
      ($Result_bsq_nothing 0)
      ($Result_BRational 0)
      ($Result_bsq_regex 0)
      ($Result_BString 0)
      ($Result_BStringPos 0)
      ($Result_BUUID 0)
      ;;NO DATA;;
    ) (
    ( ($Result_BTerm@success ($Result_BTerm@success_value BTerm)) ($Result_BTerm@error ($Result_BTerm@error_value ErrorID)) )
    ( ($Result_BBigInt@success ($Result_BBigInt@success_value BBigInt)) ($Result_BBigInt@error ($Result_BBigInt@error_value ErrorID)) )
    ( ($Result_BBigNat@success ($Result_BBigNat@success_value BBigNat)) ($Result_BBigNat@error ($Result_BBigNat@error_value ErrorID)) )
    ( ($Result_Bool@success ($Result_Bool@success_value Bool)) ($Result_Bool@error ($Result_Bool@error_value ErrorID)) )
    ( ($Result_BByteBuffer@success ($Result_BByteBuffer@success_value BByteBuffer)) ($Result_BByteBuffer@error ($Result_BByteBuffer@error_value ErrorID)) )
    ( ($Result_BHash@success ($Result_BHash@success_value BHash)) ($Result_BHash@error ($Result_BHash@error_value ErrorID)) )
    ( ($Result_BDecimal@success ($Result_BDecimal@success_value BDecimal)) ($Result_BDecimal@error ($Result_BDecimal@error_value ErrorID)) )
    ( ($Result_BFloat@success ($Result_BFloat@success_value BFloat)) ($Result_BFloat@error ($Result_BFloat@error_value ErrorID)) )
    ( ($Result_HavocSequence@success ($Result_HavocSequence@success_value HavocSequence)) ($Result_HavocSequence@error ($Result_HavocSequence@error_value ErrorID)) )
    ( ($Result_BInt@success ($Result_BInt@success_value BInt)) ($Result_BInt@error ($Result_BInt@error_value ErrorID)) )
    ( ($Result_BISOTime@success ($Result_BISOTime@success_value BISOTime)) ($Result_BISOTime@error ($Result_BISOTime@error_value ErrorID)) )
    ( ($Result_BKey@success ($Result_BKey@success_value BKey)) ($Result_BKey@error ($Result_BKey@error_value ErrorID)) )
    ( ($Result_List_Int_@success ($Result_List_Int_@success_value List_Int_)) ($Result_List_Int_@error ($Result_List_Int_@error_value ErrorID)) )
    ( ($Result_ListConcatOps@success ($Result_ListConcatOps@success_value ListConcatOps)) ($Result_ListConcatOps@error ($Result_ListConcatOps@error_value ErrorID)) )
    ( ($Result_ListFlatOps@success ($Result_ListFlatOps@success_value ListFlatOps)) ($Result_ListFlatOps@error ($Result_ListFlatOps@error_value ErrorID)) )
    ( ($Result_ListOps@success ($Result_ListOps@success_value ListOps)) ($Result_ListOps@error ($Result_ListOps@error_value ErrorID)) )
    ( ($Result_BLogicalTime@success ($Result_BLogicalTime@success_value BLogicalTime)) ($Result_BLogicalTime@error ($Result_BLogicalTime@error_value ErrorID)) )
    ( ($Result_BNat@success ($Result_BNat@success_value BNat)) ($Result_BNat@error ($Result_BNat@error_value ErrorID)) )
    ( ($Result_bsq_none@success ($Result_bsq_none@success_value bsq_none)) ($Result_bsq_none@error ($Result_bsq_none@error_value ErrorID)) )
    ( ($Result_bsq_nothing@success ($Result_bsq_nothing@success_value bsq_nothing)) ($Result_bsq_nothing@error ($Result_bsq_nothing@error_value ErrorID)) )
    ( ($Result_BRational@success ($Result_BRational@success_value BRational)) ($Result_BRational@error ($Result_BRational@error_value ErrorID)) )
    ( ($Result_bsq_regex@success ($Result_bsq_regex@success_value bsq_regex)) ($Result_bsq_regex@error ($Result_bsq_regex@error_value ErrorID)) )
    ( ($Result_BString@success ($Result_BString@success_value BString)) ($Result_BString@error ($Result_BString@error_value ErrorID)) )
    ( ($Result_BStringPos@success ($Result_BStringPos@success_value BStringPos)) ($Result_BStringPos@error ($Result_BStringPos@error_value ErrorID)) )
    ( ($Result_BUUID@success ($Result_BUUID@success_value BUUID)) ($Result_BUUID@error ($Result_BUUID@error_value ErrorID)) )
    ;;NO DATA;;
))

;;
;;Free constructors for entrypoint initialization
;;
(define-fun BNone@UFCons_API ((hs (Seq BNat))) bsq_none
  bsq_none@literal
)

(define-fun BNothing@UFCons_API ((hs (Seq BNat))) bsq_nothing
  bsq_nothing@literal
)

(declare-fun BBool@UFCons_API ((Seq BNat)) Bool)
(declare-fun BInt@UFCons_API ((Seq BNat)) BInt )
(declare-fun BNat@UFCons_API ((Seq BNat)) BNat)
(declare-fun BBigInt@UFCons_API ((Seq BNat)) BBigInt)
(declare-fun BBigNat@UFCons_API ((Seq BNat)) BBigNat)
(declare-fun BFloat@UFCons_API ((Seq BNat)) BFloat)
(declare-fun BDecimal@UFCons_API ((Seq BNat)) BDecimal)
(declare-fun BRational@UFCons_API ((Seq BNat)) BRational)
(declare-fun BString@UFCons_API ((Seq BNat)) BString)
(declare-fun BByteBuffer@UFCons_API ((Seq BNat)) BByteBuffer)
(declare-fun BISOTime@UFCons_API ((Seq BNat)) BISOTime)
(declare-fun BLogicalTime@UFCons_API ((Seq BNat)) BLogicalTime)
(declare-fun BUUID@UFCons_API ((Seq BNat)) BUUID)
(declare-fun BContentHash@UFCons_API ((Seq BNat)) BHash)

(declare-fun ListSize@UFCons_API ((Seq BNat)) BNat)
(declare-fun EnumChoice@UFCons_API ((Seq BNat)) BNat)
(declare-fun ConceptChoice@UFCons_API ((Seq BNat)) BNat)
(declare-fun UnionChoice@UFCons_API ((Seq BNat)) BNat)

;;NO DATA;;

;;NO DATA;;

(define-fun _@@consop_List_Int__list_1 ((_0_ BInt)) List_Int_
(List_Int_@cons (_ bv1 8) (_@@cons_List_Int__list_1 _0_))
)

(define-fun ListFlatOps..s_empty__ ((l List_Int_)) Bool
(= l List_Int_@empty_const)
)

(define-fun ListOps..s_and2 ((b1 Bool) (b2 Bool)) Bool
(and b1 b2)
)

(define-fun ListOps..s_size__ ((l List_Int_)) BNat
(List_Int_@size l)
)

(define-fun _@@consop_List_Int__concat2 ((l1 List_Int_) (l2 List_Int_) (count BNat)) List_Int_
(List_Int_@cons count (_@@cons_List_Int__concat2 l1 l2))
)

(define-fun ListOps..s_concat2_impl__ ((l1 List_Int_) (l2 List_Int_) (count BNat)) List_Int_
(_@@consop_List_Int__concat2 l1 l2 count)
)

(define-fun ListOps..s_concat2__ ((l1 List_Int_) (l2 List_Int_)) $Result_List_Int_
(let ((@tmp_0 (ListFlatOps..s_empty__ l1)))
    (let ((l1empty @tmp_0))
      (let ((@tmp_2 (ListFlatOps..s_empty__ l2)))
        (let ((l2empty @tmp_2))
          (let ((@tmp_4 (ListOps..s_and2 @tmp_0 @tmp_2)))
            (ite @tmp_4
              (let ((@tmp_7 List_Int_@empty_const))
                (let (($__ir_ret__$3 @tmp_7))
                  (let (($__ir_ret__$4 $__ir_ret__$3))
                    (let (($return $__ir_ret__$4))
                      ($Result_List_Int_@success $return)
                    )
                  )
                )
              )
              (ite l1empty
                (let (($__ir_ret__$2 l2))
                  (let (($__ir_ret__$4 $__ir_ret__$2))
                    (let (($return $__ir_ret__$4))
                      ($Result_List_Int_@success $return)
                    )
                  )
                )
                (ite l2empty
                  (let (($__ir_ret__$1 l1))
                    (let (($__ir_ret__$4 $__ir_ret__$1))
                      (let (($return $__ir_ret__$4))
                        ($Result_List_Int_@success $return)
                      )
                    )
                  )
                  (let ((@tmp_12 (ListOps..s_size__ l1)))
                    (let ((l1size @tmp_12))
                      (let ((@tmp_14 (ListOps..s_size__ l2)))
                        (let ((l2size @tmp_14))
                          (let ((_@tmpvar@0 (ite (bvugt (bvadd ((_ zero_extend 1) @tmp_12) ((_ zero_extend 1) @tmp_14)) (_ bv255 9)) ($Result_BNat@error ErrorID_AssumeCheck) ($Result_BNat@success (bvadd @tmp_12 @tmp_14)))))
                            (ite ((_ is $Result_BNat@error) _@tmpvar@0)
                              ($Result_List_Int_@error ($Result_BNat@error_value _@tmpvar@0))
                              (let ((@tmp_16 ($Result_BNat@success_value _@tmpvar@0)))
                                (let ((ncount @tmp_16))
                                  (let ((@tmp_19 (ListOps..s_concat2_impl__ l1 l2 @tmp_16)))
                                    (let (($__ir_ret__ @tmp_19))
                                      (let (($__ir_ret__$4 $__ir_ret__))
                                        (let (($return $__ir_ret__$4))
                                          ($Result_List_Int_@success $return)
                                        )
                                      )
                                    )
                                  )
                                )
                              )
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)

(define-fun List_Int_..pushBack__ ((this List_Int_) (v BInt)) $Result_List_Int_
(let ((@tmp_2 (_@@consop_List_Int__list_1 v)))
    (let ((_@tmpvar@1 (ListOps..s_concat2__ this @tmp_2)))
      (ite ((_ is $Result_List_Int_@error) _@tmpvar@1)
        _@tmpvar@1
        (let ((@tmp_0 ($Result_List_Int_@success_value _@tmpvar@1)))
          (let (($__ir_ret__ @tmp_0))
            (let (($return $__ir_ret__))
              ($Result_List_Int_@success $return)
            )
          )
        )
      )
    )
  )
)

(define-fun ListFlatOps..s_isFlatList__ ((l List_Int_)) Bool
(or (= l List_Int_@empty_const) ((_ is _@@cons_List_Int__list_1) (List_Int_@uli l)) ((_ is _@@cons_List_Int__list_2) (List_Int_@uli l)) ((_ is _@@cons_List_Int__list_3) (List_Int_@uli l)))
)

(define-fun ListFlatOps..s_is1__ ((l List_Int_)) Bool
((_ is _@@cons_List_Int__list_1) (List_Int_@uli l))
)

(define-fun ListFlatOps..s_1at0__ ((l List_Int_)) BInt
(_@@cons_List_Int__list_1__0_ (List_Int_@uli l))
)

(define-fun pred--C._Users_marron_Desktop_doit.bsq_k8..31@839 ((x BInt)) Bool
(let ((@tmp_0 (bvsge x BInt@zero)))
    (let (($__ir_ret__ @tmp_0))
      (let (($return $__ir_ret__))
        $return
      )
    )
  )
)

(define-fun pred--list.bsq_k1..238@7435 ((v BInt)) Bool
(let ((@tmp_1 (pred--C._Users_marron_Desktop_doit.bsq_k8..31@839 v)))
    (let ((@tmp_0 (not @tmp_1)))
      (let (($__ir_ret__ @tmp_0))
        (let (($return $__ir_ret__))
          $return
        )
      )
    )
  )
)

(define-fun ListFlatOps..s_has_pred_1___pred--list.bsq_k1..238@7435_ ((l List_Int_)) Bool
(let ((@tmp_1 (ListFlatOps..s_1at0__ l)))
    (let ((@tmp_0 (pred--list.bsq_k1..238@7435 @tmp_1)))
      (let (($__ir_ret__ @tmp_0))
        (let (($return $__ir_ret__))
          $return
        )
      )
    )
  )
)

(define-fun ListFlatOps..s_is2__ ((l List_Int_)) Bool
((_ is _@@cons_List_Int__list_2) (List_Int_@uli l))
)

(define-fun ListFlatOps..s_2at0__ ((l List_Int_)) BInt
(_@@cons_List_Int__list_2__0_ (List_Int_@uli l))
)

(define-fun ListFlatOps..s_2at1__ ((l List_Int_)) BInt
(_@@cons_List_Int__list_2__1_ (List_Int_@uli l))
)

(define-fun ListOps..s_or2 ((b1 Bool) (b2 Bool)) Bool
(or b1 b2)
)

(define-fun ListFlatOps..s_has_pred_2___pred--list.bsq_k1..238@7435_ ((l List_Int_)) Bool
(let ((@tmp_2 (ListFlatOps..s_2at0__ l)))
    (let ((@tmp_1 (pred--list.bsq_k1..238@7435 @tmp_2)))
      (let ((@tmp_5 (ListFlatOps..s_2at1__ l)))
        (let ((@tmp_4 (pred--list.bsq_k1..238@7435 @tmp_5)))
          (let ((@tmp_0 (ListOps..s_or2 @tmp_1 @tmp_4)))
            (let (($__ir_ret__ @tmp_0))
              (let (($return $__ir_ret__))
                $return
              )
            )
          )
        )
      )
    )
  )
)

(define-fun ListFlatOps..s_3at0__ ((l List_Int_)) BInt
(_@@cons_List_Int__list_3__0_ (List_Int_@uli l))
)

(define-fun ListFlatOps..s_3at1__ ((l List_Int_)) BInt
(_@@cons_List_Int__list_3__1_ (List_Int_@uli l))
)

(define-fun ListFlatOps..s_3at2__ ((l List_Int_)) BInt
(_@@cons_List_Int__list_3__2_ (List_Int_@uli l))
)

(define-fun ListOps..s_or3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool
(or b1 b2 b3)
)

(define-fun ListFlatOps..s_has_pred_3___pred--list.bsq_k1..238@7435_ ((l List_Int_)) Bool
(let ((@tmp_2 (ListFlatOps..s_3at0__ l)))
    (let ((@tmp_1 (pred--list.bsq_k1..238@7435 @tmp_2)))
      (let ((@tmp_5 (ListFlatOps..s_3at1__ l)))
        (let ((@tmp_4 (pred--list.bsq_k1..238@7435 @tmp_5)))
          (let ((@tmp_8 (ListFlatOps..s_3at2__ l)))
            (let ((@tmp_7 (pred--list.bsq_k1..238@7435 @tmp_8)))
              (let ((@tmp_0 (ListOps..s_or3 @tmp_1 @tmp_4 @tmp_7)))
                (let (($__ir_ret__ @tmp_0))
                  (let (($return $__ir_ret__))
                    $return
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)

(define-fun ListFlatOps..s_has_pred___pred--list.bsq_k1..238@7435_ ((l List_Int_)) Bool
(let ((@tmp_0 (ListFlatOps..s_empty__ l)))
    (ite @tmp_0
      (let (($__ir_ret__$3 false))
        (let (($__ir_ret__$4 $__ir_ret__$3))
          (let (($return $__ir_ret__$4))
            $return
          )
        )
      )
      (let ((@tmp_3 (ListFlatOps..s_is1__ l)))
        (ite @tmp_3
          (let ((@tmp_5 (ListFlatOps..s_has_pred_1___pred--list.bsq_k1..238@7435_ l)))
            (let (($__ir_ret__$2 @tmp_5))
              (let (($__ir_ret__$4 $__ir_ret__$2))
                (let (($return $__ir_ret__$4))
                  $return
                )
              )
            )
          )
          (let ((@tmp_8 (ListFlatOps..s_is2__ l)))
            (ite @tmp_8
              (let ((@tmp_10 (ListFlatOps..s_has_pred_2___pred--list.bsq_k1..238@7435_ l)))
                (let (($__ir_ret__$1 @tmp_10))
                  (let (($__ir_ret__$4 $__ir_ret__$1))
                    (let (($return $__ir_ret__$4))
                      $return
                    )
                  )
                )
              )
              (let ((@tmp_13 (ListFlatOps..s_has_pred_3___pred--list.bsq_k1..238@7435_ l)))
                (let (($__ir_ret__ @tmp_13))
                  (let (($__ir_ret__$4 $__ir_ret__))
                    (let (($return $__ir_ret__$4))
                      $return
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)

(define-fun ListConcatOps..s_isConcatList__ ((l List_Int_)) Bool
((_ is _@@cons_List_Int__concat2) (List_Int_@uli l))
)

(define-fun ListConcatOps..s_left__ ((l List_Int_)) List_Int_
(_@@cons_List_Int__concat2_left (List_Int_@uli l))
)

(define-fun _@@desop_List_Int__safeCheckPred_using_pred--list.bsq_k1..238@7435 ((l List_Int_) (count BNat)) $Result_List_Int_
($Result_List_Int_@success l)
)

(define-fun ListOps..s_safe_pred_impl___pred--list.bsq_k1..238@7435_ ((l List_Int_) (count BNat)) $Result_List_Int_
(_@@desop_List_Int__safeCheckPred_using_pred--list.bsq_k1..238@7435 l count)
)

(define-fun-rec _@@desop_List_Int__get ((l List_Int_) (n BNat)) BInt
 (let ((_@list_contents (List_Int_@uli l)))
    (ite ((_ is _@@cons_List_Int__list_1) _@list_contents)
      (_@@cons_List_Int__list_1__0_ _@list_contents)
      (ite ((_ is _@@cons_List_Int__list_2) _@list_contents)
      (ite (= n BNat@zero)
        (_@@cons_List_Int__list_2__0_ _@list_contents)
        (_@@cons_List_Int__list_2__1_ _@list_contents)
      )
      (ite ((_ is _@@cons_List_Int__list_3) _@list_contents)
      (ite (= n BNat@zero)
        (_@@cons_List_Int__list_3__0_ _@list_contents)
        (ite (= n (_ bv1 8))
        (_@@cons_List_Int__list_3__1_ _@list_contents)
        (_@@cons_List_Int__list_3__2_ _@list_contents)
      )
      )
      (ite ((_ is _@@cons_List_Int__slice) _@list_contents)
      (_@@desop_List_Int__get (_@@cons_List_Int__slice_l _@list_contents) (bvadd n (_@@cons_List_Int__slice_start _@list_contents)))
      (ite ((_ is _@@cons_List_Int__concat2) _@list_contents)
      (let ((_@l1 (_@@cons_List_Int__concat2_left _@list_contents)))
        (let ((_@l1size (List_Int_@size _@l1)))
          (ite (bvult n _@l1size)
            (_@@desop_List_Int__get _@l1 n)
            (_@@desop_List_Int__get (_@@cons_List_Int__concat2_right _@list_contents) (bvsub n _@l1size))
          )
        )
      )
      ($Result_BInt@success_value ($Result_BInt@success (BInt@UFCons_API (seq.++ (_@@cons_List_Int__havoc_path _@list_contents) (seq.unit n)))))
    )
    )
    )
    )
    )
  )
)

(define-fun _@@desop_List_Int__hasPredCheck_using_pred--list.bsq_k1..238@7435 ((l List_Int_) (count BNat)) $Result_Bool
($Result_Bool@success (exists ((_@n BNat)) (= _@n BNat@zero)))
;; ($Result_Bool@success true)
)

(define-fun ListOps..s_has_pred_impl___pred--list.bsq_k1..238@7435_ ((l List_Int_) (count BNat)) $Result_Bool
(_@@desop_List_Int__hasPredCheck_using_pred--list.bsq_k1..238@7435 l count)
)

(define-fun ListOps..s_has_pred_base___pred--list.bsq_k1..238@7435_ ((l List_Int_)) $Result_Bool
(let ((@tmp_2 (ListOps..s_size__ l)))
    (let ((_@tmpvar@3 (ListOps..s_safe_pred_impl___pred--list.bsq_k1..238@7435_ l @tmp_2)))
      (ite ((_ is $Result_List_Int_@error) _@tmpvar@3)
        ($Result_Bool@error ($Result_List_Int_@error_value _@tmpvar@3))
        (let ((@tmp_0 ($Result_List_Int_@success_value _@tmpvar@3)))
          (let ((sl @tmp_0))
            (let ((@tmp_7 (ListOps..s_size__ @tmp_0)))
              (let ((_@tmpvar@2 (ListOps..s_has_pred_impl___pred--list.bsq_k1..238@7435_ @tmp_0 @tmp_7)))
                (ite ((_ is $Result_Bool@error) _@tmpvar@2)
                  _@tmpvar@2
                  (let ((@tmp_5 ($Result_Bool@success_value _@tmpvar@2)))
                    (let (($__ir_ret__ @tmp_5))
                      (let (($return $__ir_ret__))
                        ($Result_Bool@success $return)
                      )
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)

(define-fun ListConcatOps..s_right__ ((l List_Int_)) List_Int_
(_@@cons_List_Int__concat2_right (List_Int_@uli l))
)

(define-funs-rec (
  (ListConcatOps..s_concat_lropt_has_pred___pred--list.bsq_k1..238@7435_ ((l List_Int_)) $Result_Bool)
  (ListConcatOps..s_has_pred___pred--list.bsq_k1..238@7435_ ((l List_Int_)) $Result_Bool)
) (
(let ((@tmp_0 (ListFlatOps..s_isFlatList__ l)))
    (ite @tmp_0
      (let ((@tmp_2 (ListFlatOps..s_has_pred___pred--list.bsq_k1..238@7435_ l)))
        (let (($__ir_ret__$2 @tmp_2))
          (let (($__ir_ret__$3 $__ir_ret__$2))
            (let (($return $__ir_ret__$3))
              ($Result_Bool@success $return)
            )
          )
        )
      )
      (let ((@tmp_5 (ListConcatOps..s_isConcatList__ l)))
        (ite @tmp_5
          (let ((_@tmpvar@4 (ListConcatOps..s_has_pred___pred--list.bsq_k1..238@7435_ l)))
            (ite ((_ is $Result_Bool@error) _@tmpvar@4)
              _@tmpvar@4
              (let ((@tmp_7 ($Result_Bool@success_value _@tmpvar@4)))
                (let (($__ir_ret__$1 @tmp_7))
                  (let (($__ir_ret__$3 $__ir_ret__$1))
                    (let (($return $__ir_ret__$3))
                      ($Result_Bool@success $return)
                    )
                  )
                )
              )
            )
          )
          (let ((_@tmpvar@5 (ListOps..s_has_pred_base___pred--list.bsq_k1..238@7435_ l)))
            (ite ((_ is $Result_Bool@error) _@tmpvar@5)
              _@tmpvar@5
              (let ((@tmp_10 ($Result_Bool@success_value _@tmpvar@5)))
                (let (($__ir_ret__ @tmp_10))
                  (let (($__ir_ret__$3 $__ir_ret__))
                    (let (($return $__ir_ret__$3))
                      ($Result_Bool@success $return)
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
  )
(let ((@tmp_2 (ListConcatOps..s_left__ l)))
    (let ((_@tmpvar@7 (ListConcatOps..s_concat_lropt_has_pred___pred--list.bsq_k1..238@7435_ @tmp_2)))
      (ite ((_ is $Result_Bool@error) _@tmpvar@7)
        _@tmpvar@7
        (let ((@tmp_1 ($Result_Bool@success_value _@tmpvar@7)))
          (let ((@tmp_6 (ListConcatOps..s_right__ l)))
            (let ((_@tmpvar@6 (ListConcatOps..s_concat_lropt_has_pred___pred--list.bsq_k1..238@7435_ @tmp_6)))
              (ite ((_ is $Result_Bool@error) _@tmpvar@6)
                _@tmpvar@6
                (let ((@tmp_5 ($Result_Bool@success_value _@tmpvar@6)))
                  (let ((@tmp_0 (ListOps..s_or2 @tmp_1 @tmp_5)))
                    (let (($__ir_ret__ @tmp_0))
                      (let (($return $__ir_ret__))
                        ($Result_Bool@success $return)
                      )
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
  )))

(define-fun ListOps..s_has_pred___pred--list.bsq_k1..238@7435_ ((l List_Int_)) $Result_Bool
(let ((@tmp_0 (ListFlatOps..s_empty__ l)))
    (ite @tmp_0
      (let (($__ir_ret__$3 false))
        (let (($__ir_ret__$4 $__ir_ret__$3))
          (let (($return $__ir_ret__$4))
            ($Result_Bool@success $return)
          )
        )
      )
      (let ((@tmp_3 (ListFlatOps..s_isFlatList__ l)))
        (ite @tmp_3
          (let ((@tmp_5 (ListFlatOps..s_has_pred___pred--list.bsq_k1..238@7435_ l)))
            (let (($__ir_ret__$2 @tmp_5))
              (let (($__ir_ret__$4 $__ir_ret__$2))
                (let (($return $__ir_ret__$4))
                  ($Result_Bool@success $return)
                )
              )
            )
          )
          (let ((@tmp_8 (ListConcatOps..s_isConcatList__ l)))
            (ite @tmp_8
              (let ((_@tmpvar@12 (ListConcatOps..s_has_pred___pred--list.bsq_k1..238@7435_ l)))
                (ite ((_ is $Result_Bool@error) _@tmpvar@12)
                  _@tmpvar@12
                  (let ((@tmp_10 ($Result_Bool@success_value _@tmpvar@12)))
                    (let (($__ir_ret__$1 @tmp_10))
                      (let (($__ir_ret__$4 $__ir_ret__$1))
                        (let (($return $__ir_ret__$4))
                          ($Result_Bool@success $return)
                        )
                      )
                    )
                  )
                )
              )
              (let ((_@tmpvar@13 (ListOps..s_has_pred_base___pred--list.bsq_k1..238@7435_ l)))
                (ite ((_ is $Result_Bool@error) _@tmpvar@13)
                  _@tmpvar@13
                  (let ((@tmp_13 ($Result_Bool@success_value _@tmpvar@13)))
                    (let (($__ir_ret__ @tmp_13))
                      (let (($__ir_ret__$4 $__ir_ret__))
                        (let (($return $__ir_ret__$4))
                          ($Result_Bool@success $return)
                        )
                      )
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)

(define-fun List_Int_..allOf___pred--C._Users_marron_Desktop_doit.bsq_k8..31@839_ ((this List_Int_)) $Result_Bool
(let ((_@tmpvar@14 (ListOps..s_has_pred___pred--list.bsq_k1..238@7435_ this)))
    (ite ((_ is $Result_Bool@error) _@tmpvar@14)
      _@tmpvar@14
      (let ((@tmp_1 ($Result_Bool@success_value _@tmpvar@14)))
        (let ((@tmp_0 (not @tmp_1)))
          (let (($__ir_ret__ @tmp_0))
            (let (($return $__ir_ret__))
              ($Result_Bool@success $return)
            )
          )
        )
      )
    )
  )
)

(define-fun NSMain..allPositive ((args List_Int_)) $Result_Bool
(let ((_@tmpvar@15 (List_Int_..allOf___pred--C._Users_marron_Desktop_doit.bsq_k8..31@839_ args)))
    (ite ((_ is $Result_Bool@error) _@tmpvar@15)
      _@tmpvar@15
      (let ((@tmp_2 ($Result_Bool@success_value _@tmpvar@15)))
        (let (($__ir_ret__ @tmp_2))
          (let (($return $__ir_ret__))
            ($Result_Bool@success $return)
          )
        )
      )
    )
  )
)

(define-fun NSMain..main ((l List_Int_)) $Result_Bool
(let ((_@tmpvar@17 (List_Int_..pushBack__ l #b11111111)))
    (ite ((_ is $Result_List_Int_@error) _@tmpvar@17)
      ($Result_Bool@error ($Result_List_Int_@error_value _@tmpvar@17))
      (let ((@tmp_3 ($Result_List_Int_@success_value _@tmpvar@17)))
        (let ((_@tmpvar@16 (NSMain..allPositive @tmp_3)))
          (ite ((_ is $Result_Bool@error) _@tmpvar@16)
            _@tmpvar@16
            (let ((@tmp_0 ($Result_Bool@success_value _@tmpvar@16)))
              (let ((res @tmp_0))
                (let ((@tmp_5 (not @tmp_0)))
                  (ite @tmp_5
                    (let (($__ir_ret__ @tmp_0))
                      (let (($return $__ir_ret__))
                        ($Result_Bool@success $return)
                      )
                    )
                    ($Result_Bool@error ErrorID_Target)
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)

(define-fun _@@consop_List_Int__havoc ((path HavocSequence)) $Result_List_Int_
(let ((_@size (ListSize@UFCons_API path)))
    (ite (= _@size BNat@zero)
      ($Result_List_Int_@success List_Int_@empty_const)
      (ite (forall ((_@n BNat)) (=> (bvult _@n _@size) ((_ is $Result_BInt@success) ($Result_BInt@success (BInt@UFCons_API (seq.++ path (seq.unit _@n)))))))
        ($Result_List_Int_@success (List_Int_@cons _@size (_@@cons_List_Int__havoc path)))
        ($Result_List_Int_@error ErrorID_AssumeCheck)
      )
    )
  )
)

(define-fun _@@cons_List_Int__entrypoint ((path HavocSequence)) $Result_List_Int_
(_@@consop_List_Int__havoc path)
)

;;NO DATA;;

(declare-const l $Result_List_Int_)
(assert (= l (_@@cons_List_Int__entrypoint (seq.++ (seq.unit BNat@zero) (seq.unit BNat@zero)))))
(assert ((_ is $Result_List_Int_@success) l))
(declare-const _@smtres@ $Result_Bool)
(assert (= _@smtres@ (NSMain..main ($Result_List_Int_@success_value l))))
(assert (= _@smtres@ ($Result_Bool@error ErrorID_Target)))

(check-sat)

[NikolajBjorner]

quantifiers inside recursive function definitions were not supported because the existing core required pre-processing formulas with quantifiers (it cannot handle quantifiers as arguments to terms on its own and requires a pre-processor to create proxies for the quantifiers). I have updated the recursive function solver to handle quantified definitions by introducing proxies on the fly. Your example now solves (to unsat). If you can avoid quantifiers inside recursive function definitions it also helps.