1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
** Calling: yices-smt2 --incremental
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
** Backend solver Yices does not support global decls.
** Some incremental calls, such as pop, will be limited.
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic QF_BV)
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s_2 () Bool false)
[GOOD] (define-fun s_1 () Bool true)
[GOOD] (define-fun s2 () (_ BitVec 1) #b0)
[GOOD] (define-fun s68 () (_ BitVec 32) #x00000001)
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "x"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s1 () (_ BitVec 1) ((_ extract 0 0) s0))
[GOOD] (define-fun s3 () Bool (distinct s1 s2))
[GOOD] (define-fun s4 () Bool (not s3))
[GOOD] (define-fun s5 () (_ BitVec 32) (bvmul s0 s0))
[GOOD] (define-fun s6 () (_ BitVec 32) (bvmul s5 s5))
[GOOD] (define-fun s7 () (_ BitVec 32) (bvmul s6 s6))
[GOOD] (define-fun s8 () (_ BitVec 32) (bvmul s7 s7))
[GOOD] (define-fun s9 () (_ BitVec 32) (bvmul s8 s8))
[GOOD] (define-fun s10 () (_ BitVec 32) (bvmul s9 s9))
[GOOD] (define-fun s11 () (_ BitVec 32) (bvmul s10 s10))
[GOOD] (define-fun s12 () (_ BitVec 32) (bvmul s11 s11))
[GOOD] (define-fun s13 () (_ BitVec 32) (bvmul s12 s12))
[GOOD] (define-fun s14 () (_ BitVec 32) (bvmul s13 s13))
[GOOD] (define-fun s15 () (_ BitVec 32) (bvmul s14 s14))
[GOOD] (define-fun s16 () (_ BitVec 32) (bvmul s15 s15))
[GOOD] (define-fun s17 () (_ BitVec 32) (bvmul s16 s16))
[GOOD] (define-fun s18 () (_ BitVec 32) (bvmul s17 s17))
[GOOD] (define-fun s19 () (_ BitVec 32) (bvmul s18 s18))
[GOOD] (define-fun s20 () (_ BitVec 32) (bvmul s19 s19))
[GOOD] (define-fun s21 () (_ BitVec 32) (bvmul s20 s20))
[GOOD] (define-fun s22 () (_ BitVec 32) (bvmul s21 s21))
[GOOD] (define-fun s23 () (_ BitVec 32) (bvmul s22 s22))
[GOOD] (define-fun s24 () (_ BitVec 32) (bvmul s23 s23))
[GOOD] (define-fun s25 () (_ BitVec 32) (bvmul s24 s24))
[GOOD] (define-fun s26 () (_ BitVec 32) (bvmul s25 s25))
[GOOD] (define-fun s27 () (_ BitVec 32) (bvmul s26 s26))
[GOOD] (define-fun s28 () (_ BitVec 32) (bvmul s27 s27))
[GOOD] (define-fun s29 () (_ BitVec 32) (bvmul s28 s28))
[GOOD] (define-fun s30 () (_ BitVec 32) (bvmul s29 s29))
[GOOD] (define-fun s31 () (_ BitVec 32) (bvmul s30 s30))
[GOOD] (define-fun s32 () (_ BitVec 32) (bvmul s31 s31))
[GOOD] (define-fun s33 () (_ BitVec 32) (bvmul s32 s32))
[GOOD] (define-fun s34 () (_ BitVec 32) (bvmul s33 s33))
[FAIL] (define-fun s35 () (_ BitVec 32) (bvmul s34 s34))
CAUGHT SMT EXCEPTION
*** Data.SBV: Unexpected non-success response from Yices:
***
*** Sent : (define-fun s35 () (_ BitVec 32) (bvmul s34 s34))
*** Expected : success
*** Received : (error "at line 42, column 35: in bvmul: maximal polynomial degree exceeded")
***
*** Exit code : ExitSuccess
*** Executable: /usr/local/bin/yices-smt2
*** Options : --incremental
***
*** Reason : Check solver response for further information. If your code is correct,
*** please report this as an issue either with SBV or the solver itself!
|
