blob: 18ce2b35f53536c56a50214cbcad87557bae0ed5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
; SCRUBBER: grep -v -E '(\(define-fun)'
; EXIT: 0
(set-logic ALL)
(declare-fun arr () (Array Int Int))
(define-fun A1 () Bool (<= 1 (select arr 0)))
(define-fun A2 () Bool (<= (select arr 0) (select arr 2)))
(define-fun A3 () Bool (<= (select arr 2) (+ (select arr 0) 5)))
(define-fun A4 () Bool (<= 1 (select arr 3)))
(define-fun A5 () Bool (<= (select arr 3) (select arr 1)))
(assert (and A1 A2 A3 A4 A5))
;The conjuecture is: 2 <= x+y
(get-interpol A (<= 2 (+ (select arr 2) (select arr 3))))
|
