test/regress/regress1/arith/issue7252-arith-sanity.smt2


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

; COMMAND-LINE: -q
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(assert (> 0 (* a (mod 0 b))))
(assert (or (and (> (* b d) (* 2 (+ g c))) (= g (- c)) (> (+ e c) 0)) (> f 0)))
(check-sat)