test/regress/regress1/sygus-abduct-test-ccore.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

; REQUIRES: proof
; COMMAND-LINE: --produce-abducts --sygus-core-connective
; SCRUBBER: grep -v -E '(\(define-fun)'
; EXIT: 0

(set-logic QF_UFLIRA)
(declare-fun n () Int)
(declare-fun m () Int)
(declare-fun x () Int)
(declare-fun y () Int)

(assert (>= n 1))
(assert (and (<= n x)(<= x (+ n 5))))
(assert (and (<= 1 y)(<= y m)))

(get-abduct A (not (< x y)))