Dear colleagues,
We have another issue while using CVC4 to prove some simple code in
WhyML.
For example, for the following code
use int.Int
use list.ListRich
use string.OCaml
predicate post (n: int) (result: int) =
result = 3*n
let f (n: int) : int =
ensures { post n result }
3*n
Why3 shows that the output for CVC4 is
====================> Prover: CVC4 1.7 (counterexamples)
Unknown (sat)
Counterexample suggested by the prover:
File int.mlw:
Line 409:
max_int = {int63'int => 4611686018427387903 (0x3FFFFFFFFFFFFFFF)}
Line 411:
min_int = {int63'int => -4611686018427387904 (-0x4000000000000000)}
File invalid-counterexample.mlw:
Line 10:
n = 0 (0x0)
Line 11:
n = 0 (0x0)
We looked to the input generated by Why3 for CVC4 and it check-sat in
three
different points (two in the middle and one at the end). When we pass
this
input to CVC4 it returns "sat" for the first two checks and "unsat" for
the
last one, therefore proving that the VC is valid.
If we don't use the string.OCaml library we can prove it in Why3 using
CVC4.
The input generated by Why3 for CVC4 in this case is similar to the
previous
one (only removes some assertions related with strings) and the output
generated by CVC4 is also similar to the one in the previous case,
only differ in the models produced.
We will appreciate if someone can help us understand why in the first
case Why3 says that the output for CVC4 is "unknown" and not "valid"
as in the second case.
Thank you in advance.
Best regards,
Margarita
On 20.04.2020 18:40, Julia Lawall wrote:
On Mon, 20 Apr 2020, margarita.capretto wrote:
Dear colleagues,
My name is Margarita Capretto and I am doing research with prof. Cesar
Sanchez
at the IMDEA Software Institute. We are using Why3 (and in particular
WhyML) for deductive software verification.
We have some problems trying to prove/generating counterexample for
some simple code in WhyML using CVC4 (version 1.7) and Z3 (version
4.8.6) and we'd appreciate if someone can help us understand why this
happen.
Here is a simplified example that illustrates the issue:
let function mult3 (t: uint64) : uint64 =
requires { in_bounds (3*t) }
ensures { result = 3*t }
3*t
predicate post_mult3 (n: uint64) (result: uint64) =
result = mult3 n
let f_pred_mult3 (n: uint64) : uint64 =
requires { in_bounds (3*n) }
ensures { post_mult3 n result }
3*n
The VC for the function f_pred_mult3 can be proven by Z3. However,
CVC4 runs out of time while trying to prove it but then can prove it
when it tries to get a counterexample. If we don't define any
predicate and we simply write
ensures {result = mult3 n} (see f_mult3)
or if we don't use function mult3 (see f and f_pred), then CVC4 can
prove the VC without any problem. In the attached file there are more
examples where the argument is passed in a record or the result is
returned in a list. In some of this cases, Z3 is not able to prove nor
generate counterexamples for the VCs (see f_record_list_pred and
f_list_pred) and CVC4 has the same problem as above. Seems like some
problems can be avoided if we do not use predicates, why is that? Is
there an easy way to see the input to CVC4 and Z3 generated by Why3?
At least for CVC4 (I don't use Z3), you can click on edit on the CVC4
line
and see this information. You need your editor for CVC4 to be emacs in
the preferences menu.
julia
Thank you advance.
Best regards,
Margarita
;; produced by cvc4_17_counterexample.drv ;;
;; produced by cvc4_17.drv ;;
(set-logic ALL_SUPPORTED)
;;; generated by SMT-LIB strings
(set-info :smt-lib-version 2.6)
;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
(set-option :produce-models true)
(set-option :incremental true)
;;; SMT-LIB2: integer arithmetic
(declare-sort uni 0)
(declare-sort ty 0)
(declare-fun sort (ty uni) Bool)
(declare-fun witness (ty) uni)
(declare-fun int () ty)
(declare-fun real () ty)
(declare-fun string () ty)
(declare-fun bool () ty)
(declare-fun match_bool (ty Bool uni uni) uni)
(declare-fun index_bool (Bool) Int)
(declare-sort tuple0 0)
(declare-fun tuple01 () ty)
(declare-fun Tuple0 () tuple0)
(declare-fun list (ty) ty)
(declare-fun Nil (ty) uni)
(declare-fun Cons (ty uni uni) uni)
(declare-fun match_list (ty ty uni uni uni) uni)
(declare-fun index_list (ty uni) Int)
(declare-fun Cons_proj_1 (ty uni) uni)
(declare-fun Cons_proj_2 (ty uni) uni)
(declare-fun is_nil (ty uni) Bool)
(declare-fun length (ty uni) Int)
(declare-fun mem (ty uni uni) Bool)
(declare-fun option (ty) ty)
(declare-fun None (ty) uni)
(declare-fun Some (ty uni) uni)
(declare-fun match_option (ty ty uni uni uni) uni)
(declare-fun index_option (ty uni) Int)
(declare-fun Some_proj_1 (ty uni) uni)
(declare-fun is_none (ty uni) Bool)
(declare-fun nth (ty Int uni) uni)
(declare-fun hd (ty uni) uni)
(declare-fun tl (ty uni) uni)
(declare-fun infix_plpl (ty uni uni) uni)
(declare-fun reverse (ty uni) uni)
(declare-fun rev_append (ty uni uni) uni)
(declare-fun num_occ (ty uni uni) Int)
(declare-fun permut (ty uni uni) Bool)
(declare-sort int63 0)
(declare-fun int631 () ty)
(declare-fun int63qtint (int63) Int)
(declare-fun in_bounds (Int) Bool)
(declare-fun abs1 (Int) Int)
(declare-fun div1 (Int Int) Int)
(declare-fun mod1 (Int Int) Int)
(declare-fun max_int () int63)
(declare-fun min_int () int63)
(declare-fun is_digit (String) Bool)
(declare-sort char 0)
(declare-fun char1 () ty)
(declare-fun contents (char) String)
(declare-fun code (char) Int)
(declare-fun chr (Int) char)
(declare-fun get (String Int) char)
(declare-fun eq_string (String String) Bool)
(declare-fun make (Int char) String)
(declare-fun post (Int Int) Bool)
(declare-fun n () Int)
(declare-fun n_vc_constant () Int)
(assert
;; fqtvc
;; File "/home/margarita/Desktop/invalid-counterexample.mlw", line 10,
characters 4-5
(not (post n (* 3 n))))
(check-sat)
(get-info :reason-unknown)
(get-model)
;; n_vc_axiom
(assert (= n_vc_constant n))
;; min_int'def
(assert (= (int63qtint min_int) (- 4611686018427387904)))
;; max_int'def
(assert (= (int63qtint max_int) 4611686018427387903))
;; index_bool_False
(assert (= (index_bool false) 1))
;; index_bool_True
(assert (= (index_bool true) 0))
(check-sat)
(get-info :reason-unknown)
(get-model)
;; post'def
(assert
(forall ((n1 Int) (result Int)) (= (post n1 result) (= result (* 3 n1)))))
;; make_contents
(assert
(forall ((size Int) (v char))
(=> (<= 0 size)
(forall ((i Int))
(=> (and (<= 0 i) (< i size)) (= (get (make size v) i) v))))))
;; make_length
(assert
(forall ((size Int) (v char))
(=> (<= 0 size) (= (str.len (make size v)) size))))
;; extensionality
(assert
(forall ((s1 String) (s2 String)) (=> (eq_string s1 s2) (= s1 s2))))
;; eq_string'def
(assert
(forall ((s1 String) (s2 String))
(= (eq_string s1 s2)
(and (= (str.len s1) (str.len s2))
(forall ((i Int))
(=> (and (<= 0 i) (< i (str.len s1))) (= (get s1 i) (get s2 i))))))))
;; concat_second
(assert
(forall ((s1 String) (s2 String))
(forall ((i Int))
(=> (and (<= (str.len s1) i) (< i (+ (str.len s1) (str.len s2))))
(= (get (str.++ s1 s2) i) (get s2 (- i (str.len s1))))))))
;; concat_first
(assert
(forall ((s1 String) (s2 String))
(forall ((i Int))
(=> (and (<= 0 i) (< i (str.len s1)))
(= (get (str.++ s1 s2) i) (get s1 i))))))
;; substring_get
(assert
(forall ((s String) (ofs Int) (len Int) (i Int))
(=> (and (<= 0 ofs) (<= ofs (str.len s)))
(=> (<= 0 len)
(=> (<= (+ ofs len) (str.len s))
(=> (and (<= 0 i) (< i len))
(= (get (str.substr s ofs len) i) (get s (+ ofs i)))))))))
;; get
(assert
(forall ((s String) (i Int))
(=> (and (<= 0 i) (< i (str.len s))) (= (contents (get s i)) (str.at s i)))))
;; chr_code
(assert (forall ((c char)) (= (chr (code c)) c)))
;; code_chr
(assert
(forall ((n1 Int)) (=> (and (<= 0 n1) (< n1 256)) (= (code (chr n1)) n1))))
;; code
(assert (forall ((c char)) (and (<= 0 (code c)) (< (code c) 256))))
;; char_eq
(assert
(forall ((c1 char) (c2 char))
(=> (= (contents c1) (contents c2)) (= c1 c2))))
;; char'invariant
(assert
(forall ((self char))
(! (= (str.len (contents self)) 1) :pattern ((contents self)) )))
;; is_digit'def
(assert
(forall ((s String))
(= (is_digit s)
(and (and (<= 0 (str.to.int s)) (<= (str.to.int s) 9)) (= (str.len s) 1)))))
;; concat_substring
(assert
(forall ((s String) (ofs Int) (len Int) (lenqt Int))
(=> (and (<= 0 ofs) (<= ofs (str.len s)))
(=> (<= 0 len)
(=> (<= (+ ofs len) (str.len s))
(=> (<= 0 lenqt)
(=>
(and (<= 0 (+ (+ ofs len) lenqt)) (<= (+ (+ ofs len) lenqt) (str.len s)))
(= (str.++ (str.substr s ofs len) (str.substr s (+ ofs len) lenqt))
(str.substr s ofs (+ len lenqt))))))))))
;; substring_substring
(assert
(forall ((s String) (ofs Int) (len Int) (ofsqt Int) (lenqt Int))
(=> (and (<= 0 ofs) (<= ofs (str.len s)))
(=> (<= 0 len)
(=> (<= (+ ofs len) (str.len s))
(=> (and (<= 0 ofsqt) (<= ofsqt len))
(=> (<= 0 lenqt)
(=> (<= (+ ofsqt lenqt) len)
(= (str.substr (str.substr s ofs len) ofsqt lenqt) (str.substr s (+ ofs
ofsqt) lenqt))))))))))
;; Mod_mult
(assert
(forall ((x Int) (y Int) (z Int))
(! (=> (and (< 0 x) (and (<= 0 y) (<= 0 z)))
(= (mod1 (+ (* x y) z) x) (mod1 z x))) :pattern ((mod1 (+ (* x y) z) x))
)))
;; Div_mult
(assert
(forall ((x Int) (y Int) (z Int))
(! (=> (and (< 0 x) (and (<= 0 y) (<= 0 z)))
(= (div1 (+ (* x y) z) x) (+ y (div1 z x)))) :pattern ((div1
(+ (* x y) z) x))
)))
;; Mod_inf
(assert
(forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (mod1 x y) x))))
;; Div_inf
(assert
(forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (div1 x y) 0))))
;; Mod_1
(assert (forall ((x Int)) (= (mod1 x 1) 0)))
;; Div_1
(assert (forall ((x Int)) (= (div1 x 1) x)))
;; Rounds_toward_zero
(assert
(forall ((x Int) (y Int))
(=> (not (= y 0)) (<= (abs1 (* (div1 x y) y)) (abs1 x)))))
;; Mod_sign_neg
(assert
(forall ((x Int) (y Int))
(=> (and (<= x 0) (not (= y 0))) (<= (mod1 x y) 0))))
;; Mod_sign_pos
(assert
(forall ((x Int) (y Int))
(=> (and (<= 0 x) (not (= y 0))) (<= 0 (mod1 x y)))))
;; Div_sign_neg
(assert
(forall ((x Int) (y Int)) (=> (and (<= x 0) (< 0 y)) (<= (div1 x y) 0))))
;; Div_sign_pos
(assert
(forall ((x Int) (y Int)) (=> (and (<= 0 x) (< 0 y)) (<= 0 (div1 x y)))))
;; Mod_bound
(assert
(forall ((x Int) (y Int))
(=> (not (= y 0))
(and (< (- (abs1 y)) (mod1 x y)) (< (mod1 x y) (abs1 y))))))
;; Div_bound
(assert
(forall ((x Int) (y Int))
(=> (and (<= 0 x) (< 0 y)) (and (<= 0 (div1 x y)) (<= (div1 x y) x)))))
;; Div_mod
(assert
(forall ((x Int) (y Int))
(=> (not (= y 0)) (= x (+ (* y (div1 x y)) (mod1 x y))))))
;; Abs_pos
(assert (forall ((x Int)) (<= 0 (abs1 x))))
;; Abs_le
(assert
(forall ((x Int) (y Int)) (= (<= (abs1 x) y) (and (<= (- y) x) (<= x y)))))
;; abs'def
(assert
(forall ((x Int)) (ite (<= 0 x) (= (abs1 x) x) (= (abs1 x) (- x)))))
;; extensionality
(assert
(forall ((x int63) (y int63))
(=> (= (int63qtint x) (int63qtint y)) (= x y))))
;; to_int_in_bounds
(assert (forall ((n1 int63)) (in_bounds (int63qtint n1))))
;; in_bounds'def
(assert
(forall ((n1 Int))
(= (in_bounds n1)
(and (<= (- 4611686018427387904) n1) (<= n1 4611686018427387903)))))
;; int63'axiom
(assert
(forall ((i int63))
(and (<= (- 4611686018427387904) (int63qtint i))
(<= (int63qtint i) 4611686018427387903))))
;; Permut_length
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni))
(=> (permut a l1 l2) (= (length a l1) (length a l2))))))
;; Permut_mem
(assert
(forall ((a ty))
(forall ((x uni) (l1 uni) (l2 uni))
(=> (permut a l1 l2) (=> (mem a x l1) (mem a x l2))))))
;; Permut_append_swap
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni)) (permut a (infix_plpl a l1 l2)
(infix_plpl a l2 l1)))))
;; Permut_append
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni) (k1 uni) (k2 uni))
(=> (permut a l1 k1)
(=> (permut a l2 k2) (permut a (infix_plpl a l1 l2) (infix_plpl a k1 k2)))))))
;; Permut_assoc
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni) (l3 uni)) (permut a
(infix_plpl a (infix_plpl a l1 l2) l3)
(infix_plpl a l1 (infix_plpl a l2 l3))))))
;; Permut_cons_append
(assert
(forall ((a ty))
(forall ((x uni) (l1 uni) (l2 uni)) (permut a
(infix_plpl a (Cons a x l1) l2) (infix_plpl a l1 (Cons a x l2))))))
;; Permut_swap
(assert
(forall ((a ty))
(forall ((x uni) (y uni) (l uni)) (permut a (Cons a x (Cons a y l))
(Cons a y (Cons a x l))))))
;; Permut_cons
(assert
(forall ((a ty))
(forall ((x uni) (l1 uni) (l2 uni))
(=> (permut a l1 l2) (permut a (Cons a x l1) (Cons a x l2))))))
;; Permut_trans
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni) (l3 uni))
(=> (permut a l1 l2) (=> (permut a l2 l3) (permut a l1 l3))))))
;; Permut_sym
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni)) (=> (permut a l1 l2) (permut a l2 l1)))))
;; Permut_refl
(assert (forall ((a ty)) (forall ((l uni)) (permut a l l))))
;; permut'def
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni))
(and
(=> (permut a l1 l2)
(forall ((x uni)) (= (num_occ a x l1) (num_occ a x l2))))
(=>
(forall ((x uni)) (=> (sort a x) (= (num_occ a x l1) (num_occ a x l2))))
(permut a l1 l2))))))
;; reverse_num_occ
(assert
(forall ((a ty))
(forall ((x uni) (l uni)) (= (num_occ a x l) (num_occ a x (reverse a l))))))
;; Append_Num_Occ
(assert
(forall ((a ty))
(forall ((x uni) (l1 uni) (l2 uni))
(= (num_occ a x (infix_plpl a l1 l2)) (+ (num_occ a x l1) (num_occ a x
l2))))))
;; Mem_Num_Occ
(assert
(forall ((a ty))
(forall ((x uni) (l uni)) (= (mem a x l) (< 0 (num_occ a x l))))))
;; Num_Occ_NonNeg
(assert
(forall ((a ty)) (forall ((x uni) (l uni)) (<= 0 (num_occ a x l)))))
;; num_occ'def
(assert
(forall ((a ty))
(forall ((x uni))
(=> (sort a x)
(and (= (num_occ a x (Nil a)) 0)
(forall ((y uni) (r uni))
(=> (sort a y)
(= (num_occ a x (Cons a y r)) (+ (ite (= x y) 1 0) (num_occ a x r))))))))))
;; rev_append_append_r
(assert
(forall ((a ty))
(forall ((r uni) (s uni) (t uni))
(= (rev_append a r (infix_plpl a s t)) (rev_append a (rev_append a s r) t)))))
;; rev_append_def
(assert
(forall ((a ty))
(forall ((r uni) (s uni))
(= (rev_append a r s) (infix_plpl a (reverse a r) s)))))
;; rev_append_length
(assert
(forall ((a ty))
(forall ((s uni) (t uni))
(= (length a (rev_append a s t)) (+ (length a s) (length a t))))))
;; rev_append_append_l
(assert
(forall ((a ty))
(forall ((r uni) (s uni) (t uni))
(= (rev_append a (infix_plpl a r s) t) (rev_append a s (rev_append a r t))))))
;; rev_append'def
(assert
(forall ((a ty))
(forall ((t uni))
(and (= (rev_append a (Nil a) t) t)
(forall ((x uni) (r uni))
(= (rev_append a (Cons a x r) t) (rev_append a r (Cons a x t))))))))
;; rev_append_sort
(assert
(forall ((a ty))
(forall ((x uni) (x1 uni)) (sort (list a) (rev_append a x x1)))))
;; Reverse_length
(assert
(forall ((a ty))
(forall ((l uni)) (= (length a (reverse a l)) (length a l)))))
;; reverse_mem
(assert
(forall ((a ty))
(forall ((l uni) (x uni)) (= (mem a x l) (mem a x (reverse a l))))))
;; reverse_reverse
(assert
(forall ((a ty)) (forall ((l uni)) (= (reverse a (reverse a l)) l))))
;; cons_reverse
(assert
(forall ((a ty))
(forall ((l uni) (x uni))
(= (Cons a x (reverse a l)) (reverse a (infix_plpl a l (Cons a x (Nil
a))))))))
;; reverse_cons
(assert
(forall ((a ty))
(forall ((l uni) (x uni))
(= (reverse a (Cons a x l)) (infix_plpl a (reverse a l) (Cons a x (Nil
a)))))))
;; reverse_append
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni) (x uni))
(= (infix_plpl a (reverse a (Cons a x l1)) l2) (infix_plpl a (reverse a l1)
(Cons a x l2))))))
;; reverse'def
(assert
(forall ((a ty))
(and (= (reverse a (Nil a)) (Nil a))
(forall ((x uni) (r uni))
(= (reverse a (Cons a x r)) (infix_plpl a (reverse a r) (Cons a x (Nil
a))))))))
;; reverse_sort
(assert (forall ((a ty)) (forall ((x uni)) (sort (list a) (reverse a x)))))
;; mem_decomp
(assert
(forall ((a ty))
(forall ((x uni) (l uni))
(=> (mem a x l)
(exists ((l1 uni) (l2 uni))
(and (sort (list a) l1)
(and (sort (list a) l2) (= l (infix_plpl a l1 (Cons a x l2))))))))))
;; mem_append
(assert
(forall ((a ty))
(forall ((x uni) (l1 uni) (l2 uni))
(= (mem a x (infix_plpl a l1 l2)) (or (mem a x l1) (mem a x l2))))))
;; Append_length
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni))
(= (length a (infix_plpl a l1 l2)) (+ (length a l1) (length a l2))))))
;; Append_l_nil
(assert
(forall ((a ty)) (forall ((l uni)) (= (infix_plpl a l (Nil a)) l))))
;; Append_assoc
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni) (l3 uni))
(= (infix_plpl a l1 (infix_plpl a l2 l3)) (infix_plpl a
(infix_plpl a l1 l2) l3)))))
;; infix ++'def
(assert
(forall ((a ty))
(forall ((l2 uni))
(and (= (infix_plpl a (Nil a) l2) l2)
(forall ((x1 uni) (r1 uni))
(= (infix_plpl a (Cons a x1 r1) l2) (Cons a x1 (infix_plpl a r1 l2))))))))
;; infix ++_sort
(assert
(forall ((a ty))
(forall ((x uni) (x1 uni)) (sort (list a) (infix_plpl a x x1)))))
;; Nth0_head
(assert (forall ((a ty)) (forall ((l uni)) (= (nth a 0 l) (hd a l)))))
;; Nth_tl
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni))
(=> (= (tl a l1) (Some (list a) l2))
(forall ((i Int))
(=> (not (= i (- 1))) (= (nth a i l2) (nth a (+ i 1) l1))))))))
;; tl'def
(assert
(forall ((a ty))
(and (= (tl a (Nil a)) (None (list a)))
(forall ((x uni) (x1 uni)) (= (tl a (Cons a x x1)) (Some (list a) x1))))))
;; tl_sort
(assert
(forall ((a ty)) (forall ((x uni)) (sort (option (list a)) (tl a x)))))
;; hd'def
(assert
(forall ((a ty))
(and (= (hd a (Nil a)) (None a))
(forall ((x uni) (x1 uni)) (= (hd a (Cons a x x1)) (Some a x))))))
;; hd_sort
(assert (forall ((a ty)) (forall ((x uni)) (sort (option a) (hd a x)))))
;; nth'def
(assert
(forall ((a ty))
(forall ((n1 Int))
(and (= (nth a n1 (Nil a)) (None a))
(forall ((x uni) (r uni))
(let ((l (Cons a x r)))
(ite (= n1 0) (= (nth a n1 l) (Some a x))
(= (nth a n1 l) (nth a (- n1 1) r)))))))))
;; nth_sort
(assert
(forall ((a ty))
(forall ((x Int) (x1 uni)) (sort (option a) (nth a x x1)))))
;; is_none'spec
(assert
(forall ((a ty))
(forall ((o uni))
(=> (sort (option a) o) (= (is_none a o) (= o (None a)))))))
;; is_none'def
(assert
(forall ((a ty))
(and (is_none a (None a)) (forall ((x uni)) (not (is_none a (Some a x)))))))
;; option_inversion
(assert
(forall ((a ty))
(forall ((u uni))
(=> (sort (option a) u)
(or (= u (None a)) (= u (Some a (Some_proj_1 a u))))))))
;; Some_proj_1'def
(assert
(forall ((a ty))
(forall ((u uni)) (=> (sort a u) (= (Some_proj_1 a (Some a u)) u)))))
;; Some_proj_1_sort
(assert (forall ((a ty)) (forall ((x uni)) (sort a (Some_proj_1 a x)))))
;; index_option_Some
(assert
(forall ((a ty))
(forall ((u uni))
(! (= (index_option a (Some a u)) 1) :pattern ((Some a u)) ))))
;; index_option_None
(assert (forall ((a ty)) (= (index_option a (None a)) 0)))
;; match_option_Some
(assert
(forall ((a ty) (a1 ty))
(forall ((z uni) (z1 uni) (u uni))
(=> (sort a1 z1) (= (match_option a1 a (Some a u) z z1) z1)))))
;; match_option_None
(assert
(forall ((a ty) (a1 ty))
(forall ((z uni) (z1 uni))
(=> (sort a1 z) (= (match_option a1 a (None a) z z1) z)))))
;; match_option_sort
(assert
(forall ((a ty) (a1 ty))
(forall ((x uni) (x1 uni) (x2 uni)) (sort a1 (match_option a1 a x x1 x2)))))
;; Some_sort
(assert (forall ((a ty)) (forall ((x uni)) (sort (option a) (Some a x)))))
;; None_sort
(assert (forall ((a ty)) (sort (option a) (None a))))
;; mem'def
(assert
(forall ((a ty))
(forall ((x uni))
(=> (sort a x)
(and (not (mem a x (Nil a)))
(forall ((y uni) (r uni))
(=> (sort a y) (= (mem a x (Cons a y r)) (or (= x y) (mem a x r))))))))))
;; Length_nil
(assert
(forall ((a ty)) (forall ((l uni)) (= (= (length a l) 0) (= l (Nil a))))))
;; Length_nonnegative
(assert (forall ((a ty)) (forall ((l uni)) (<= 0 (length a l)))))
;; length'def
(assert
(forall ((a ty))
(and (= (length a (Nil a)) 0)
(forall ((x uni) (x1 uni))
(= (length a (Cons a x x1)) (+ 1 (length a x1)))))))
;; is_nil'spec
(assert
(forall ((a ty)) (forall ((l uni)) (= (is_nil a l) (= l (Nil a))))))
;; is_nil'def
(assert
(forall ((a ty))
(and (is_nil a (Nil a))
(forall ((x uni) (x1 uni)) (not (is_nil a (Cons a x x1)))))))
;; list_inversion
(assert
(forall ((a ty))
(forall ((u uni))
(or (= u (Nil a)) (= u (Cons a (Cons_proj_1 a u) (Cons_proj_2 a u)))))))
;; Cons_proj_2'def
(assert
(forall ((a ty))
(forall ((u uni) (u1 uni)) (= (Cons_proj_2 a (Cons a u u1)) u1))))
;; Cons_proj_2_sort
(assert
(forall ((a ty)) (forall ((x uni)) (sort (list a) (Cons_proj_2 a x)))))
;; Cons_proj_1'def
(assert
(forall ((a ty))
(forall ((u uni) (u1 uni))
(=> (sort a u) (= (Cons_proj_1 a (Cons a u u1)) u)))))
;; Cons_proj_1_sort
(assert (forall ((a ty)) (forall ((x uni)) (sort a (Cons_proj_1 a x)))))
;; index_list_Cons
(assert
(forall ((a ty))
(forall ((u uni) (u1 uni))
(! (= (index_list a (Cons a u u1)) 1) :pattern ((Cons a u u1)) ))))
;; index_list_Nil
(assert (forall ((a ty)) (= (index_list a (Nil a)) 0)))
;; match_list_Cons
(assert
(forall ((a ty) (a1 ty))
(forall ((z uni) (z1 uni) (u uni) (u1 uni))
(=> (sort a1 z1) (= (match_list a1 a (Cons a u u1) z z1) z1)))))
;; match_list_Nil
(assert
(forall ((a ty) (a1 ty))
(forall ((z uni) (z1 uni))
(=> (sort a1 z) (= (match_list a1 a (Nil a) z z1) z)))))
;; match_list_sort
(assert
(forall ((a ty) (a1 ty))
(forall ((x uni) (x1 uni) (x2 uni)) (sort a1 (match_list a1 a x x1 x2)))))
;; Cons_sort
(assert
(forall ((a ty)) (forall ((x uni) (x1 uni)) (sort (list a) (Cons a x x1)))))
;; Nil_sort
(assert (forall ((a ty)) (sort (list a) (Nil a))))
;; CompatOrderMult
(assert
(forall ((x Int) (y Int) (z Int))
(=> (<= x y) (=> (<= 0 z) (<= (* x z) (* y z))))))
;; tuple0_inversion
(assert (forall ((u tuple0)) (= u Tuple0)))
;; bool_inversion
(assert (forall ((u Bool)) (or (= u true) (= u false))))
;; match_bool_False
(assert
(forall ((a ty))
(forall ((z uni) (z1 uni))
(=> (sort a z1) (= (match_bool a false z z1) z1)))))
;; match_bool_True
(assert
(forall ((a ty))
(forall ((z uni) (z1 uni)) (=> (sort a z) (= (match_bool a true z z1) z)))))
;; match_bool_sort
(assert
(forall ((a ty))
(forall ((x Bool) (x1 uni) (x2 uni)) (sort a (match_bool a x x1 x2)))))
;; witness_sort
(assert (forall ((a ty)) (sort a (witness a))))
(check-sat)
(get-info :reason-unknown)
(get-model)
;; produced by cvc4_17_counterexample.drv ;;
;; produced by cvc4_17.drv ;;
(set-logic ALL_SUPPORTED)
;;; generated by SMT-LIB strings
(set-info :smt-lib-version 2.6)
;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
(set-option :produce-models true)
(set-option :incremental true)
;;; SMT-LIB2: integer arithmetic
(declare-sort uni 0)
(declare-sort ty 0)
(declare-fun sort (ty uni) Bool)
(declare-fun witness (ty) uni)
(declare-fun int () ty)
(declare-fun real () ty)
(declare-fun string () ty)
(declare-fun bool () ty)
(declare-fun match_bool (ty Bool uni uni) uni)
(declare-fun index_bool (Bool) Int)
(declare-sort tuple0 0)
(declare-fun tuple01 () ty)
(declare-fun Tuple0 () tuple0)
(declare-fun list (ty) ty)
(declare-fun Nil (ty) uni)
(declare-fun Cons (ty uni uni) uni)
(declare-fun match_list (ty ty uni uni uni) uni)
(declare-fun index_list (ty uni) Int)
(declare-fun Cons_proj_1 (ty uni) uni)
(declare-fun Cons_proj_2 (ty uni) uni)
(declare-fun is_nil (ty uni) Bool)
(declare-fun length (ty uni) Int)
(declare-fun mem (ty uni uni) Bool)
(declare-fun option (ty) ty)
(declare-fun None (ty) uni)
(declare-fun Some (ty uni) uni)
(declare-fun match_option (ty ty uni uni uni) uni)
(declare-fun index_option (ty uni) Int)
(declare-fun Some_proj_1 (ty uni) uni)
(declare-fun is_none (ty uni) Bool)
(declare-fun nth (ty Int uni) uni)
(declare-fun hd (ty uni) uni)
(declare-fun tl (ty uni) uni)
(declare-fun infix_plpl (ty uni uni) uni)
(declare-fun reverse (ty uni) uni)
(declare-fun rev_append (ty uni uni) uni)
(declare-fun num_occ (ty uni uni) Int)
(declare-fun permut (ty uni uni) Bool)
(declare-fun post (Int Int) Bool)
(declare-fun n () Int)
(declare-fun n_vc_constant () Int)
(assert
;; fqtvc
;; File "/home/margarita/Desktop/invalid-counterexample.mlw", line 10,
characters 4-5
(not (post n (* 3 n))))
(check-sat)
(get-info :reason-unknown)
(get-model)
;; n_vc_axiom
(assert (= n_vc_constant n))
;; index_bool_False
(assert (= (index_bool false) 1))
;; index_bool_True
(assert (= (index_bool true) 0))
(check-sat)
(get-info :reason-unknown)
(get-model)
;; post'def
(assert
(forall ((n1 Int) (result Int)) (= (post n1 result) (= result (* 3 n1)))))
;; Permut_length
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni))
(=> (permut a l1 l2) (= (length a l1) (length a l2))))))
;; Permut_mem
(assert
(forall ((a ty))
(forall ((x uni) (l1 uni) (l2 uni))
(=> (permut a l1 l2) (=> (mem a x l1) (mem a x l2))))))
;; Permut_append_swap
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni)) (permut a (infix_plpl a l1 l2)
(infix_plpl a l2 l1)))))
;; Permut_append
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni) (k1 uni) (k2 uni))
(=> (permut a l1 k1)
(=> (permut a l2 k2) (permut a (infix_plpl a l1 l2) (infix_plpl a k1 k2)))))))
;; Permut_assoc
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni) (l3 uni)) (permut a
(infix_plpl a (infix_plpl a l1 l2) l3)
(infix_plpl a l1 (infix_plpl a l2 l3))))))
;; Permut_cons_append
(assert
(forall ((a ty))
(forall ((x uni) (l1 uni) (l2 uni)) (permut a
(infix_plpl a (Cons a x l1) l2) (infix_plpl a l1 (Cons a x l2))))))
;; Permut_swap
(assert
(forall ((a ty))
(forall ((x uni) (y uni) (l uni)) (permut a (Cons a x (Cons a y l))
(Cons a y (Cons a x l))))))
;; Permut_cons
(assert
(forall ((a ty))
(forall ((x uni) (l1 uni) (l2 uni))
(=> (permut a l1 l2) (permut a (Cons a x l1) (Cons a x l2))))))
;; Permut_trans
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni) (l3 uni))
(=> (permut a l1 l2) (=> (permut a l2 l3) (permut a l1 l3))))))
;; Permut_sym
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni)) (=> (permut a l1 l2) (permut a l2 l1)))))
;; Permut_refl
(assert (forall ((a ty)) (forall ((l uni)) (permut a l l))))
;; permut'def
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni))
(and
(=> (permut a l1 l2)
(forall ((x uni)) (= (num_occ a x l1) (num_occ a x l2))))
(=>
(forall ((x uni)) (=> (sort a x) (= (num_occ a x l1) (num_occ a x l2))))
(permut a l1 l2))))))
;; reverse_num_occ
(assert
(forall ((a ty))
(forall ((x uni) (l uni)) (= (num_occ a x l) (num_occ a x (reverse a l))))))
;; Append_Num_Occ
(assert
(forall ((a ty))
(forall ((x uni) (l1 uni) (l2 uni))
(= (num_occ a x (infix_plpl a l1 l2)) (+ (num_occ a x l1) (num_occ a x
l2))))))
;; Mem_Num_Occ
(assert
(forall ((a ty))
(forall ((x uni) (l uni)) (= (mem a x l) (< 0 (num_occ a x l))))))
;; Num_Occ_NonNeg
(assert
(forall ((a ty)) (forall ((x uni) (l uni)) (<= 0 (num_occ a x l)))))
;; num_occ'def
(assert
(forall ((a ty))
(forall ((x uni))
(=> (sort a x)
(and (= (num_occ a x (Nil a)) 0)
(forall ((y uni) (r uni))
(=> (sort a y)
(= (num_occ a x (Cons a y r)) (+ (ite (= x y) 1 0) (num_occ a x r))))))))))
;; rev_append_append_r
(assert
(forall ((a ty))
(forall ((r uni) (s uni) (t uni))
(= (rev_append a r (infix_plpl a s t)) (rev_append a (rev_append a s r) t)))))
;; rev_append_def
(assert
(forall ((a ty))
(forall ((r uni) (s uni))
(= (rev_append a r s) (infix_plpl a (reverse a r) s)))))
;; rev_append_length
(assert
(forall ((a ty))
(forall ((s uni) (t uni))
(= (length a (rev_append a s t)) (+ (length a s) (length a t))))))
;; rev_append_append_l
(assert
(forall ((a ty))
(forall ((r uni) (s uni) (t uni))
(= (rev_append a (infix_plpl a r s) t) (rev_append a s (rev_append a r t))))))
;; rev_append'def
(assert
(forall ((a ty))
(forall ((t uni))
(and (= (rev_append a (Nil a) t) t)
(forall ((x uni) (r uni))
(= (rev_append a (Cons a x r) t) (rev_append a r (Cons a x t))))))))
;; rev_append_sort
(assert
(forall ((a ty))
(forall ((x uni) (x1 uni)) (sort (list a) (rev_append a x x1)))))
;; Reverse_length
(assert
(forall ((a ty))
(forall ((l uni)) (= (length a (reverse a l)) (length a l)))))
;; reverse_mem
(assert
(forall ((a ty))
(forall ((l uni) (x uni)) (= (mem a x l) (mem a x (reverse a l))))))
;; reverse_reverse
(assert
(forall ((a ty)) (forall ((l uni)) (= (reverse a (reverse a l)) l))))
;; cons_reverse
(assert
(forall ((a ty))
(forall ((l uni) (x uni))
(= (Cons a x (reverse a l)) (reverse a (infix_plpl a l (Cons a x (Nil
a))))))))
;; reverse_cons
(assert
(forall ((a ty))
(forall ((l uni) (x uni))
(= (reverse a (Cons a x l)) (infix_plpl a (reverse a l) (Cons a x (Nil
a)))))))
;; reverse_append
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni) (x uni))
(= (infix_plpl a (reverse a (Cons a x l1)) l2) (infix_plpl a (reverse a l1)
(Cons a x l2))))))
;; reverse'def
(assert
(forall ((a ty))
(and (= (reverse a (Nil a)) (Nil a))
(forall ((x uni) (r uni))
(= (reverse a (Cons a x r)) (infix_plpl a (reverse a r) (Cons a x (Nil
a))))))))
;; reverse_sort
(assert (forall ((a ty)) (forall ((x uni)) (sort (list a) (reverse a x)))))
;; mem_decomp
(assert
(forall ((a ty))
(forall ((x uni) (l uni))
(=> (mem a x l)
(exists ((l1 uni) (l2 uni))
(and (sort (list a) l1)
(and (sort (list a) l2) (= l (infix_plpl a l1 (Cons a x l2))))))))))
;; mem_append
(assert
(forall ((a ty))
(forall ((x uni) (l1 uni) (l2 uni))
(= (mem a x (infix_plpl a l1 l2)) (or (mem a x l1) (mem a x l2))))))
;; Append_length
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni))
(= (length a (infix_plpl a l1 l2)) (+ (length a l1) (length a l2))))))
;; Append_l_nil
(assert
(forall ((a ty)) (forall ((l uni)) (= (infix_plpl a l (Nil a)) l))))
;; Append_assoc
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni) (l3 uni))
(= (infix_plpl a l1 (infix_plpl a l2 l3)) (infix_plpl a
(infix_plpl a l1 l2) l3)))))
;; infix ++'def
(assert
(forall ((a ty))
(forall ((l2 uni))
(and (= (infix_plpl a (Nil a) l2) l2)
(forall ((x1 uni) (r1 uni))
(= (infix_plpl a (Cons a x1 r1) l2) (Cons a x1 (infix_plpl a r1 l2))))))))
;; infix ++_sort
(assert
(forall ((a ty))
(forall ((x uni) (x1 uni)) (sort (list a) (infix_plpl a x x1)))))
;; Nth0_head
(assert (forall ((a ty)) (forall ((l uni)) (= (nth a 0 l) (hd a l)))))
;; Nth_tl
(assert
(forall ((a ty))
(forall ((l1 uni) (l2 uni))
(=> (= (tl a l1) (Some (list a) l2))
(forall ((i Int))
(=> (not (= i (- 1))) (= (nth a i l2) (nth a (+ i 1) l1))))))))
;; tl'def
(assert
(forall ((a ty))
(and (= (tl a (Nil a)) (None (list a)))
(forall ((x uni) (x1 uni)) (= (tl a (Cons a x x1)) (Some (list a) x1))))))
;; tl_sort
(assert
(forall ((a ty)) (forall ((x uni)) (sort (option (list a)) (tl a x)))))
;; hd'def
(assert
(forall ((a ty))
(and (= (hd a (Nil a)) (None a))
(forall ((x uni) (x1 uni)) (= (hd a (Cons a x x1)) (Some a x))))))
;; hd_sort
(assert (forall ((a ty)) (forall ((x uni)) (sort (option a) (hd a x)))))
;; nth'def
(assert
(forall ((a ty))
(forall ((n1 Int))
(and (= (nth a n1 (Nil a)) (None a))
(forall ((x uni) (r uni))
(let ((l (Cons a x r)))
(ite (= n1 0) (= (nth a n1 l) (Some a x))
(= (nth a n1 l) (nth a (- n1 1) r)))))))))
;; nth_sort
(assert
(forall ((a ty))
(forall ((x Int) (x1 uni)) (sort (option a) (nth a x x1)))))
;; is_none'spec
(assert
(forall ((a ty))
(forall ((o uni))
(=> (sort (option a) o) (= (is_none a o) (= o (None a)))))))
;; is_none'def
(assert
(forall ((a ty))
(and (is_none a (None a)) (forall ((x uni)) (not (is_none a (Some a x)))))))
;; option_inversion
(assert
(forall ((a ty))
(forall ((u uni))
(=> (sort (option a) u)
(or (= u (None a)) (= u (Some a (Some_proj_1 a u))))))))
;; Some_proj_1'def
(assert
(forall ((a ty))
(forall ((u uni)) (=> (sort a u) (= (Some_proj_1 a (Some a u)) u)))))
;; Some_proj_1_sort
(assert (forall ((a ty)) (forall ((x uni)) (sort a (Some_proj_1 a x)))))
;; index_option_Some
(assert
(forall ((a ty))
(forall ((u uni))
(! (= (index_option a (Some a u)) 1) :pattern ((Some a u)) ))))
;; index_option_None
(assert (forall ((a ty)) (= (index_option a (None a)) 0)))
;; match_option_Some
(assert
(forall ((a ty) (a1 ty))
(forall ((z uni) (z1 uni) (u uni))
(=> (sort a1 z1) (= (match_option a1 a (Some a u) z z1) z1)))))
;; match_option_None
(assert
(forall ((a ty) (a1 ty))
(forall ((z uni) (z1 uni))
(=> (sort a1 z) (= (match_option a1 a (None a) z z1) z)))))
;; match_option_sort
(assert
(forall ((a ty) (a1 ty))
(forall ((x uni) (x1 uni) (x2 uni)) (sort a1 (match_option a1 a x x1 x2)))))
;; Some_sort
(assert (forall ((a ty)) (forall ((x uni)) (sort (option a) (Some a x)))))
;; None_sort
(assert (forall ((a ty)) (sort (option a) (None a))))
;; mem'def
(assert
(forall ((a ty))
(forall ((x uni))
(=> (sort a x)
(and (not (mem a x (Nil a)))
(forall ((y uni) (r uni))
(=> (sort a y) (= (mem a x (Cons a y r)) (or (= x y) (mem a x r))))))))))
;; Length_nil
(assert
(forall ((a ty)) (forall ((l uni)) (= (= (length a l) 0) (= l (Nil a))))))
;; Length_nonnegative
(assert (forall ((a ty)) (forall ((l uni)) (<= 0 (length a l)))))
;; length'def
(assert
(forall ((a ty))
(and (= (length a (Nil a)) 0)
(forall ((x uni) (x1 uni))
(= (length a (Cons a x x1)) (+ 1 (length a x1)))))))
;; is_nil'spec
(assert
(forall ((a ty)) (forall ((l uni)) (= (is_nil a l) (= l (Nil a))))))
;; is_nil'def
(assert
(forall ((a ty))
(and (is_nil a (Nil a))
(forall ((x uni) (x1 uni)) (not (is_nil a (Cons a x x1)))))))
;; list_inversion
(assert
(forall ((a ty))
(forall ((u uni))
(or (= u (Nil a)) (= u (Cons a (Cons_proj_1 a u) (Cons_proj_2 a u)))))))
;; Cons_proj_2'def
(assert
(forall ((a ty))
(forall ((u uni) (u1 uni)) (= (Cons_proj_2 a (Cons a u u1)) u1))))
;; Cons_proj_2_sort
(assert
(forall ((a ty)) (forall ((x uni)) (sort (list a) (Cons_proj_2 a x)))))
;; Cons_proj_1'def
(assert
(forall ((a ty))
(forall ((u uni) (u1 uni))
(=> (sort a u) (= (Cons_proj_1 a (Cons a u u1)) u)))))
;; Cons_proj_1_sort
(assert (forall ((a ty)) (forall ((x uni)) (sort a (Cons_proj_1 a x)))))
;; index_list_Cons
(assert
(forall ((a ty))
(forall ((u uni) (u1 uni))
(! (= (index_list a (Cons a u u1)) 1) :pattern ((Cons a u u1)) ))))
;; index_list_Nil
(assert (forall ((a ty)) (= (index_list a (Nil a)) 0)))
;; match_list_Cons
(assert
(forall ((a ty) (a1 ty))
(forall ((z uni) (z1 uni) (u uni) (u1 uni))
(=> (sort a1 z1) (= (match_list a1 a (Cons a u u1) z z1) z1)))))
;; match_list_Nil
(assert
(forall ((a ty) (a1 ty))
(forall ((z uni) (z1 uni))
(=> (sort a1 z) (= (match_list a1 a (Nil a) z z1) z)))))
;; match_list_sort
(assert
(forall ((a ty) (a1 ty))
(forall ((x uni) (x1 uni) (x2 uni)) (sort a1 (match_list a1 a x x1 x2)))))
;; Cons_sort
(assert
(forall ((a ty)) (forall ((x uni) (x1 uni)) (sort (list a) (Cons a x x1)))))
;; Nil_sort
(assert (forall ((a ty)) (sort (list a) (Nil a))))
;; CompatOrderMult
(assert
(forall ((x Int) (y Int) (z Int))
(=> (<= x y) (=> (<= 0 z) (<= (* x z) (* y z))))))
;; tuple0_inversion
(assert (forall ((u tuple0)) (= u Tuple0)))
;; bool_inversion
(assert (forall ((u Bool)) (or (= u true) (= u false))))
;; match_bool_False
(assert
(forall ((a ty))
(forall ((z uni) (z1 uni))
(=> (sort a z1) (= (match_bool a false z z1) z1)))))
;; match_bool_True
(assert
(forall ((a ty))
(forall ((z uni) (z1 uni)) (=> (sort a z) (= (match_bool a true z z1) z)))))
;; match_bool_sort
(assert
(forall ((a ty))
(forall ((x Bool) (x1 uni) (x2 uni)) (sort a (match_bool a x x1 x2)))))
;; witness_sort
(assert (forall ((a ty)) (sort a (witness a))))
(check-sat)
(get-info :reason-unknown)
(get-model)
module InvalidCounterexample
use int.Int
use list.ListRich
(*use string.OCaml*)
predicate post (n: int) (result: int) =
result = 3*n
let f (n: int) : int =
ensures { post n result }
3*n
(*
====================> Prover: CVC4 1.7 (counterexamples)
Unknown (sat)
Counterexample suggested by the prover:
File int.mlw:
Line 409:
max_int = {int63'int => 4611686018427387903 (0x3FFFFFFFFFFFFFFF)}
Line 411:
min_int = {int63'int => -4611686018427387904 (-0x4000000000000000)}
File invalid-counterexample.mlw:
Line 10:
n = 0 (0x0)
Line 11:
n = 0 (0x0)
*)
endsat
(error "Can't get-info :reason-unknown when the last result wasn't unknown!")
(model
(declare-sort uni 0)
(declare-sort ty 0)
(define-fun sort ((BOUND_VARIABLE_379 ty) (BOUND_VARIABLE_380 uni)) Bool false)
(define-fun witness ((BOUND_VARIABLE_391 ty)) uni @uc_uni_0)
(define-fun int () ty @uc_ty_0)
(define-fun real () ty @uc_ty_0)
(define-fun string () ty @uc_ty_0)
(define-fun bool () ty @uc_ty_0)
(define-fun match_bool ((BOUND_VARIABLE_415 ty) (BOUND_VARIABLE_416 Bool)
(BOUND_VARIABLE_417 uni) (BOUND_VARIABLE_418 uni)) uni @uc_uni_0)
(define-fun index_bool ((BOUND_VARIABLE_432 Bool)) Int 0)
(declare-sort tuple0 0)
(define-fun tuple01 () ty @uc_ty_0)
(define-fun Tuple0 () tuple0 @uc_tuple0_0)
(define-fun list ((BOUND_VARIABLE_441 ty)) ty @uc_ty_0)
(define-fun Nil ((BOUND_VARIABLE_391 ty)) uni @uc_uni_0)
(define-fun Cons ((BOUND_VARIABLE_458 ty) (BOUND_VARIABLE_459 uni)
(BOUND_VARIABLE_460 uni)) uni @uc_uni_0)
(define-fun match_list ((BOUND_VARIABLE_488 ty) (BOUND_VARIABLE_489 ty)
(BOUND_VARIABLE_490 uni) (BOUND_VARIABLE_491 uni) (BOUND_VARIABLE_492 uni)) uni
@uc_uni_0)
(define-fun index_list ((BOUND_VARIABLE_513 ty) (BOUND_VARIABLE_514 uni)) Int 0)
(define-fun Cons_proj_1 ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni
@uc_uni_0)
(define-fun Cons_proj_2 ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni
@uc_uni_0)
(define-fun is_nil ((BOUND_VARIABLE_379 ty) (BOUND_VARIABLE_380 uni)) Bool
false)
(define-fun length ((BOUND_VARIABLE_513 ty) (BOUND_VARIABLE_514 uni)) Int 0)
(define-fun mem ((BOUND_VARIABLE_564 ty) (BOUND_VARIABLE_565 uni)
(BOUND_VARIABLE_566 uni)) Bool false)
(define-fun option ((BOUND_VARIABLE_441 ty)) ty @uc_ty_0)
(define-fun None ((BOUND_VARIABLE_391 ty)) uni @uc_uni_0)
(define-fun Some ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni
@uc_uni_0)
(define-fun match_option ((BOUND_VARIABLE_488 ty) (BOUND_VARIABLE_489 ty)
(BOUND_VARIABLE_490 uni) (BOUND_VARIABLE_491 uni) (BOUND_VARIABLE_492 uni)) uni
@uc_uni_0)
(define-fun index_option ((BOUND_VARIABLE_513 ty) (BOUND_VARIABLE_514 uni)) Int
0)
(define-fun Some_proj_1 ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni
@uc_uni_0)
(define-fun is_none ((BOUND_VARIABLE_379 ty) (BOUND_VARIABLE_380 uni)) Bool
false)
(define-fun nth ((BOUND_VARIABLE_631 ty) (BOUND_VARIABLE_632 Int)
(BOUND_VARIABLE_633 uni)) uni @uc_uni_0)
(define-fun hd ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni @uc_uni_0)
(define-fun tl ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni @uc_uni_0)
(define-fun infix_plpl ((BOUND_VARIABLE_458 ty) (BOUND_VARIABLE_459 uni)
(BOUND_VARIABLE_460 uni)) uni @uc_uni_0)
(define-fun reverse ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni
@uc_uni_0)
(define-fun rev_append ((BOUND_VARIABLE_458 ty) (BOUND_VARIABLE_459 uni)
(BOUND_VARIABLE_460 uni)) uni @uc_uni_0)
(define-fun num_occ ((BOUND_VARIABLE_689 ty) (BOUND_VARIABLE_690 uni)
(BOUND_VARIABLE_691 uni)) Int 0)
(define-fun permut ((BOUND_VARIABLE_564 ty) (BOUND_VARIABLE_565 uni)
(BOUND_VARIABLE_566 uni)) Bool false)
(declare-sort int63 0)
(define-fun int631 () ty @uc_ty_0)
(define-fun int63qtint ((BOUND_VARIABLE_712 int63)) Int 0)
(define-fun in_bounds ((BOUND_VARIABLE_720 Int)) Bool false)
(define-fun abs1 ((BOUND_VARIABLE_728 Int)) Int 0)
(define-fun div1 ((BOUND_VARIABLE_739 Int) (BOUND_VARIABLE_740 Int)) Int 0)
(define-fun mod1 ((BOUND_VARIABLE_739 Int) (BOUND_VARIABLE_740 Int)) Int 0)
(define-fun max_int () int63 @uc_int63_0)
(define-fun min_int () int63 @uc_int63_0)
(define-fun is_digit ((BOUND_VARIABLE_757 String)) Bool false)
(declare-sort char 0)
(define-fun char1 () ty @uc_ty_0)
(define-fun contents ((BOUND_VARIABLE_765 char)) String "")
(define-fun code ((BOUND_VARIABLE_773 char)) Int 0)
(define-fun chr ((BOUND_VARIABLE_782 Int)) char @uc_char_0)
(define-fun get ((BOUND_VARIABLE_793 String) (BOUND_VARIABLE_794 Int)) char
@uc_char_0)
(define-fun eq_string ((BOUND_VARIABLE_807 String) (BOUND_VARIABLE_808 String))
Bool false)
(define-fun make ((BOUND_VARIABLE_821 Int) (BOUND_VARIABLE_822 char)) String "")
(define-fun post ((BOUND_VARIABLE_831 Int) (BOUND_VARIABLE_832 Int)) Bool false)
(define-fun n () Int 0)
(define-fun n_vc_constant () Int 0)
)
sat
(error "Can't get-info :reason-unknown when the last result wasn't unknown!")
(model
(declare-sort uni 0)
(declare-sort ty 0)
(define-fun sort ((BOUND_VARIABLE_379 ty) (BOUND_VARIABLE_380 uni)) Bool false)
(define-fun witness ((BOUND_VARIABLE_391 ty)) uni @uc_uni_0)
(define-fun int () ty @uc_ty_0)
(define-fun real () ty @uc_ty_0)
(define-fun string () ty @uc_ty_0)
(define-fun bool () ty @uc_ty_0)
(define-fun match_bool ((BOUND_VARIABLE_415 ty) (BOUND_VARIABLE_416 Bool)
(BOUND_VARIABLE_417 uni) (BOUND_VARIABLE_418 uni)) uni @uc_uni_0)
(define-fun index_bool ((_arg_index_bool_1 Bool)) Int (ite (not
_arg_index_bool_1) 1 0))
(declare-sort tuple0 0)
(define-fun tuple01 () ty @uc_ty_0)
(define-fun Tuple0 () tuple0 @uc_tuple0_0)
(define-fun list ((BOUND_VARIABLE_441 ty)) ty @uc_ty_0)
(define-fun Nil ((BOUND_VARIABLE_391 ty)) uni @uc_uni_0)
(define-fun Cons ((BOUND_VARIABLE_458 ty) (BOUND_VARIABLE_459 uni)
(BOUND_VARIABLE_460 uni)) uni @uc_uni_0)
(define-fun match_list ((BOUND_VARIABLE_488 ty) (BOUND_VARIABLE_489 ty)
(BOUND_VARIABLE_490 uni) (BOUND_VARIABLE_491 uni) (BOUND_VARIABLE_492 uni)) uni
@uc_uni_0)
(define-fun index_list ((BOUND_VARIABLE_513 ty) (BOUND_VARIABLE_514 uni)) Int 0)
(define-fun Cons_proj_1 ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni
@uc_uni_0)
(define-fun Cons_proj_2 ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni
@uc_uni_0)
(define-fun is_nil ((BOUND_VARIABLE_379 ty) (BOUND_VARIABLE_380 uni)) Bool
false)
(define-fun length ((BOUND_VARIABLE_513 ty) (BOUND_VARIABLE_514 uni)) Int 0)
(define-fun mem ((BOUND_VARIABLE_564 ty) (BOUND_VARIABLE_565 uni)
(BOUND_VARIABLE_566 uni)) Bool false)
(define-fun option ((BOUND_VARIABLE_441 ty)) ty @uc_ty_0)
(define-fun None ((BOUND_VARIABLE_391 ty)) uni @uc_uni_0)
(define-fun Some ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni
@uc_uni_0)
(define-fun match_option ((BOUND_VARIABLE_488 ty) (BOUND_VARIABLE_489 ty)
(BOUND_VARIABLE_490 uni) (BOUND_VARIABLE_491 uni) (BOUND_VARIABLE_492 uni)) uni
@uc_uni_0)
(define-fun index_option ((BOUND_VARIABLE_513 ty) (BOUND_VARIABLE_514 uni)) Int
0)
(define-fun Some_proj_1 ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni
@uc_uni_0)
(define-fun is_none ((BOUND_VARIABLE_379 ty) (BOUND_VARIABLE_380 uni)) Bool
false)
(define-fun nth ((BOUND_VARIABLE_631 ty) (BOUND_VARIABLE_632 Int)
(BOUND_VARIABLE_633 uni)) uni @uc_uni_0)
(define-fun hd ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni @uc_uni_0)
(define-fun tl ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni @uc_uni_0)
(define-fun infix_plpl ((BOUND_VARIABLE_458 ty) (BOUND_VARIABLE_459 uni)
(BOUND_VARIABLE_460 uni)) uni @uc_uni_0)
(define-fun reverse ((BOUND_VARIABLE_527 ty) (BOUND_VARIABLE_528 uni)) uni
@uc_uni_0)
(define-fun rev_append ((BOUND_VARIABLE_458 ty) (BOUND_VARIABLE_459 uni)
(BOUND_VARIABLE_460 uni)) uni @uc_uni_0)
(define-fun num_occ ((BOUND_VARIABLE_689 ty) (BOUND_VARIABLE_690 uni)
(BOUND_VARIABLE_691 uni)) Int 0)
(define-fun permut ((BOUND_VARIABLE_564 ty) (BOUND_VARIABLE_565 uni)
(BOUND_VARIABLE_566 uni)) Bool false)
; cardinality of int63 is 2
(declare-sort int63 0)
; rep: @uc_int63_0
; rep: @uc_int63_1
(define-fun int631 () ty @uc_ty_0)
(define-fun int63qtint ((BOUND_VARIABLE_712 int63)) Int (ite (=
BOUND_VARIABLE_712 @uc_int63_1) (- 4611686018427387904) 4611686018427387903))
(define-fun in_bounds ((BOUND_VARIABLE_720 Int)) Bool false)
(define-fun abs1 ((BOUND_VARIABLE_728 Int)) Int 0)
(define-fun div1 ((BOUND_VARIABLE_739 Int) (BOUND_VARIABLE_740 Int)) Int 0)
(define-fun mod1 ((BOUND_VARIABLE_739 Int) (BOUND_VARIABLE_740 Int)) Int 0)
(define-fun max_int () int63 @uc_int63_0)
(define-fun min_int () int63 @uc_int63_1)
(define-fun is_digit ((BOUND_VARIABLE_757 String)) Bool false)
(declare-sort char 0)
(define-fun char1 () ty @uc_ty_0)
(define-fun contents ((BOUND_VARIABLE_765 char)) String "")
(define-fun code ((BOUND_VARIABLE_773 char)) Int 0)
(define-fun chr ((BOUND_VARIABLE_782 Int)) char @uc_char_0)
(define-fun get ((BOUND_VARIABLE_793 String) (BOUND_VARIABLE_794 Int)) char
@uc_char_0)
(define-fun eq_string ((BOUND_VARIABLE_807 String) (BOUND_VARIABLE_808 String))
Bool false)
(define-fun make ((BOUND_VARIABLE_821 Int) (BOUND_VARIABLE_822 char)) String "")
(define-fun post ((BOUND_VARIABLE_831 Int) (BOUND_VARIABLE_832 Int)) Bool false)
(define-fun n () Int 0)
(define-fun n_vc_constant () Int 0)
)
unsat
(error "Can't get-info :reason-unknown when the last result wasn't unknown!")
(error "Cannot get the current model unless immediately preceded by SAT/INVALID
or UNKNOWN response.")
sat
(error "Can't get-info :reason-unknown when the last result wasn't unknown!")
(model
(declare-sort uni 0)
(declare-sort ty 0)
(define-fun sort ((BOUND_VARIABLE_348 ty) (BOUND_VARIABLE_349 uni)) Bool false)
(define-fun witness ((BOUND_VARIABLE_360 ty)) uni @uc_uni_0)
(define-fun int () ty @uc_ty_0)
(define-fun real () ty @uc_ty_0)
(define-fun string () ty @uc_ty_0)
(define-fun bool () ty @uc_ty_0)
(define-fun match_bool ((BOUND_VARIABLE_384 ty) (BOUND_VARIABLE_385 Bool)
(BOUND_VARIABLE_386 uni) (BOUND_VARIABLE_387 uni)) uni @uc_uni_0)
(define-fun index_bool ((BOUND_VARIABLE_401 Bool)) Int 0)
(declare-sort tuple0 0)
(define-fun tuple01 () ty @uc_ty_0)
(define-fun Tuple0 () tuple0 @uc_tuple0_0)
(define-fun list ((BOUND_VARIABLE_410 ty)) ty @uc_ty_0)
(define-fun Nil ((BOUND_VARIABLE_360 ty)) uni @uc_uni_0)
(define-fun Cons ((BOUND_VARIABLE_427 ty) (BOUND_VARIABLE_428 uni)
(BOUND_VARIABLE_429 uni)) uni @uc_uni_0)
(define-fun match_list ((BOUND_VARIABLE_457 ty) (BOUND_VARIABLE_458 ty)
(BOUND_VARIABLE_459 uni) (BOUND_VARIABLE_460 uni) (BOUND_VARIABLE_461 uni)) uni
@uc_uni_0)
(define-fun index_list ((BOUND_VARIABLE_482 ty) (BOUND_VARIABLE_483 uni)) Int 0)
(define-fun Cons_proj_1 ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni
@uc_uni_0)
(define-fun Cons_proj_2 ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni
@uc_uni_0)
(define-fun is_nil ((BOUND_VARIABLE_348 ty) (BOUND_VARIABLE_349 uni)) Bool
false)
(define-fun length ((BOUND_VARIABLE_482 ty) (BOUND_VARIABLE_483 uni)) Int 0)
(define-fun mem ((BOUND_VARIABLE_533 ty) (BOUND_VARIABLE_534 uni)
(BOUND_VARIABLE_535 uni)) Bool false)
(define-fun option ((BOUND_VARIABLE_410 ty)) ty @uc_ty_0)
(define-fun None ((BOUND_VARIABLE_360 ty)) uni @uc_uni_0)
(define-fun Some ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni
@uc_uni_0)
(define-fun match_option ((BOUND_VARIABLE_457 ty) (BOUND_VARIABLE_458 ty)
(BOUND_VARIABLE_459 uni) (BOUND_VARIABLE_460 uni) (BOUND_VARIABLE_461 uni)) uni
@uc_uni_0)
(define-fun index_option ((BOUND_VARIABLE_482 ty) (BOUND_VARIABLE_483 uni)) Int
0)
(define-fun Some_proj_1 ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni
@uc_uni_0)
(define-fun is_none ((BOUND_VARIABLE_348 ty) (BOUND_VARIABLE_349 uni)) Bool
false)
(define-fun nth ((BOUND_VARIABLE_600 ty) (BOUND_VARIABLE_601 Int)
(BOUND_VARIABLE_602 uni)) uni @uc_uni_0)
(define-fun hd ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni @uc_uni_0)
(define-fun tl ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni @uc_uni_0)
(define-fun infix_plpl ((BOUND_VARIABLE_427 ty) (BOUND_VARIABLE_428 uni)
(BOUND_VARIABLE_429 uni)) uni @uc_uni_0)
(define-fun reverse ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni
@uc_uni_0)
(define-fun rev_append ((BOUND_VARIABLE_427 ty) (BOUND_VARIABLE_428 uni)
(BOUND_VARIABLE_429 uni)) uni @uc_uni_0)
(define-fun num_occ ((BOUND_VARIABLE_658 ty) (BOUND_VARIABLE_659 uni)
(BOUND_VARIABLE_660 uni)) Int 0)
(define-fun permut ((BOUND_VARIABLE_533 ty) (BOUND_VARIABLE_534 uni)
(BOUND_VARIABLE_535 uni)) Bool false)
(define-fun post ((BOUND_VARIABLE_682 Int) (BOUND_VARIABLE_683 Int)) Bool false)
(define-fun n () Int 0)
(define-fun n_vc_constant () Int 0)
)
sat
(error "Can't get-info :reason-unknown when the last result wasn't unknown!")
(model
(declare-sort uni 0)
(declare-sort ty 0)
(define-fun sort ((BOUND_VARIABLE_348 ty) (BOUND_VARIABLE_349 uni)) Bool false)
(define-fun witness ((BOUND_VARIABLE_360 ty)) uni @uc_uni_0)
(define-fun int () ty @uc_ty_0)
(define-fun real () ty @uc_ty_0)
(define-fun string () ty @uc_ty_0)
(define-fun bool () ty @uc_ty_0)
(define-fun match_bool ((BOUND_VARIABLE_384 ty) (BOUND_VARIABLE_385 Bool)
(BOUND_VARIABLE_386 uni) (BOUND_VARIABLE_387 uni)) uni @uc_uni_0)
(define-fun index_bool ((_arg_index_bool_1 Bool)) Int (ite (not
_arg_index_bool_1) 1 0))
(declare-sort tuple0 0)
(define-fun tuple01 () ty @uc_ty_0)
(define-fun Tuple0 () tuple0 @uc_tuple0_0)
(define-fun list ((BOUND_VARIABLE_410 ty)) ty @uc_ty_0)
(define-fun Nil ((BOUND_VARIABLE_360 ty)) uni @uc_uni_0)
(define-fun Cons ((BOUND_VARIABLE_427 ty) (BOUND_VARIABLE_428 uni)
(BOUND_VARIABLE_429 uni)) uni @uc_uni_0)
(define-fun match_list ((BOUND_VARIABLE_457 ty) (BOUND_VARIABLE_458 ty)
(BOUND_VARIABLE_459 uni) (BOUND_VARIABLE_460 uni) (BOUND_VARIABLE_461 uni)) uni
@uc_uni_0)
(define-fun index_list ((BOUND_VARIABLE_482 ty) (BOUND_VARIABLE_483 uni)) Int 0)
(define-fun Cons_proj_1 ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni
@uc_uni_0)
(define-fun Cons_proj_2 ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni
@uc_uni_0)
(define-fun is_nil ((BOUND_VARIABLE_348 ty) (BOUND_VARIABLE_349 uni)) Bool
false)
(define-fun length ((BOUND_VARIABLE_482 ty) (BOUND_VARIABLE_483 uni)) Int 0)
(define-fun mem ((BOUND_VARIABLE_533 ty) (BOUND_VARIABLE_534 uni)
(BOUND_VARIABLE_535 uni)) Bool false)
(define-fun option ((BOUND_VARIABLE_410 ty)) ty @uc_ty_0)
(define-fun None ((BOUND_VARIABLE_360 ty)) uni @uc_uni_0)
(define-fun Some ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni
@uc_uni_0)
(define-fun match_option ((BOUND_VARIABLE_457 ty) (BOUND_VARIABLE_458 ty)
(BOUND_VARIABLE_459 uni) (BOUND_VARIABLE_460 uni) (BOUND_VARIABLE_461 uni)) uni
@uc_uni_0)
(define-fun index_option ((BOUND_VARIABLE_482 ty) (BOUND_VARIABLE_483 uni)) Int
0)
(define-fun Some_proj_1 ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni
@uc_uni_0)
(define-fun is_none ((BOUND_VARIABLE_348 ty) (BOUND_VARIABLE_349 uni)) Bool
false)
(define-fun nth ((BOUND_VARIABLE_600 ty) (BOUND_VARIABLE_601 Int)
(BOUND_VARIABLE_602 uni)) uni @uc_uni_0)
(define-fun hd ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni @uc_uni_0)
(define-fun tl ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni @uc_uni_0)
(define-fun infix_plpl ((BOUND_VARIABLE_427 ty) (BOUND_VARIABLE_428 uni)
(BOUND_VARIABLE_429 uni)) uni @uc_uni_0)
(define-fun reverse ((BOUND_VARIABLE_496 ty) (BOUND_VARIABLE_497 uni)) uni
@uc_uni_0)
(define-fun rev_append ((BOUND_VARIABLE_427 ty) (BOUND_VARIABLE_428 uni)
(BOUND_VARIABLE_429 uni)) uni @uc_uni_0)
(define-fun num_occ ((BOUND_VARIABLE_658 ty) (BOUND_VARIABLE_659 uni)
(BOUND_VARIABLE_660 uni)) Int 0)
(define-fun permut ((BOUND_VARIABLE_533 ty) (BOUND_VARIABLE_534 uni)
(BOUND_VARIABLE_535 uni)) Bool false)
(define-fun post ((BOUND_VARIABLE_682 Int) (BOUND_VARIABLE_683 Int)) Bool false)
(define-fun n () Int 0)
(define-fun n_vc_constant () Int 0)
)
unsat
(error "Can't get-info :reason-unknown when the last result wasn't unknown!")
(error "Cannot get the current model unless immediately preceded by SAT/INVALID
or UNKNOWN response.")
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
