test/regress/regress1/quantifiers/qe-partial.smt2


1
2
3
4
5
6
7
8
9

; COMMAND-LINE:
; SCRUBBER: sed -e 's/(not (>= (+ .* (\* (- 1) .*)) 1))$/(not (>= (+ TERMA (\* (- 1) TERMB)) 1))/'
; EXPECT: (not (>= (+ TERMA (* (- 1) TERMB)) 1))
(set-logic LIA)
(set-info :status unsat)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(get-qe-disjunct (exists ((x Int)) (and (<= a x) (or (<= x b) (<= x c)))))