blob: 1aa900bfc7ac39f6066a8551d65808e4701a72ad (
plain)
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
|
unsat
(check
;; Declarations
(% x (term Int)
(% A1 (th_holds true)
(% A0 (th_holds (not (impl (= Int (-_Int x (a_int 3) ) (a_int 7) ) (<=_Int (a_int 10) x) )))
(: (holds cln)
;; Printing deferred declarations
;; BV const letification
;; Printing the global let map
(@ let1 false
;; Printing aliasing declarations
;; Rewrites for Lemmas
;; In the preprocessor we trust
(th_let_pf _ (trust_f false) (\ .PA205
(th_let_pf _ (trust_f (not let1)) (\ .PA227
;; Printing mapping from preprocessed assertions into atoms
(decl_atom let1 (\ .v1 (\ .a1
(satlem _ _ (ast _ _ _ .a1 (\ .l3 (clausify_false (contra _ .l3 .PA227)))) (\ .pb1
(satlem _ _ (asf _ _ _ .a1 (\ .l2 (clausify_false (contra _ .PA205 .l2)))) (\ .pb4
;; Theory Lemmas
;; BB atom mapping
;; Bit-blasting definitional clauses
;; Bit-blasting learned clauses
(satlem_simplify _ _ _ (R _ _ .pb4 .pb1 .v1) (\ empty empty)))))))))))))))))))
;;
|
