test/regress/cli/regress0/bug605.cvc.smt2

   1 ; EXPECT: sat
   2 (set-logic ALL)
   3 (set-option :incremental true)
   4 (set-option :produce-models true)
   5 (declare-datatypes ((__cvc5_record_longitude_Int_latitude_Int 0)) (((__cvc5_record_longitude_Int_latitude_Int_ctor (longitude Int) (latitude Int)))))
   6
   7 (declare-datatypes ((|__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)| 0)) (((|__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_ctor| (geoLoc (Set __cvc5_record_longitude_Int_latitude_Int))))))
   8
   9 (declare-datatypes ((|__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_| 0)) (((|__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__ctor| (base |__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)|)))))
  10
  11 (declare-datatypes ((|__cvc5_record_s_f____cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__| 0)) (((|__cvc5_record_s_f____cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)___ctor| (s_f |__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_|)))))
  12
  13
  14 (declare-fun a () (Array Int |__cvc5_record_s_f____cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__|))
  15 (define-fun p1 () __cvc5_record_longitude_Int_latitude_Int (__cvc5_record_longitude_Int_latitude_Int_ctor 0 0))
  16 (define-fun s1 () |__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)| (|__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_ctor| (set.singleton (__cvc5_record_longitude_Int_latitude_Int_ctor 0 0))))
  17 (define-fun f0 () |__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_| (|__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__ctor| (|__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_ctor| (set.singleton (__cvc5_record_longitude_Int_latitude_Int_ctor 0 0)))))
  18 (define-fun init ((v (Array Int |__cvc5_record_s_f____cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__|)) (i Int) (f |__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_|)) Bool (= (s_f (select v 0)) f))
  19 (assert (init a 2 (|__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__ctor| (|__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_ctor| (set.singleton (__cvc5_record_longitude_Int_latitude_Int_ctor 0 0))))))
  20 (push 1)
  21
  22 (assert true)
  23
  24 (check-sat)
  25
  26 (pop 1)
  27