blob: 9bcb93476fa8ff32405437e61f6403b04c9a8613 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n)
; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
; EXPECT: The fact in question: (>= (+ (* (- 1) (/ n n)) termITE_132) 0)
; EXPECT: ")
; EXIT: 1
(set-logic QF_LRA)
(set-info :status unknown)
(declare-fun n () Real)
; This example is test that LRA rejects multiplication terms
(assert (= (/ n n) 1))
(check-sat)
|
