smt.arith.solver=6 Assertion violation at ../src/smt/theory_lra.cpp Line: 989

[muchang]

Hi,
For this formula:

(declare-fun HTSab_new () Real) 
(declare-fun ECxis_new () Real )  
(declare-fun a () Real) 
(declare-fun b () Real) 
(declare-fun UAfuP_new () Real) 
(declare-fun c () Real) 
(declare-fun d () Real) 
(declare-fun Jlidu_new () Real) 
(declare-fun x () Real) 
(declare-fun e () Real) 
(declare-fun ehbTa_new () Real) 
(declare-fun f () Real) 
(declare-fun y () Real) 
(declare-fun CLPEA_new () Real) 
(declare-fun g () Real) 
(declare-fun h () Real) 
(declare-fun i () Real) 
(declare-fun j () Real) 
(declare-fun t1428uscore0 () Real) 
(declare-fun B () Real) 
(declare-fun v2 () Real) 
(declare-fun k () Real) 
(declare-fun l () Real) 
(declare-fun I2 () Real) 
(declare-fun m () Real) 
(declare-fun V () Real) 
(declare-fun n () Real) 
(declare-fun o () Real) 
(declare-fun aa () Real) 
(declare-fun z () Real) 
(declare-fun A_shifted () Real) 
(declare-fun p () Real) 
(declare-fun q () Real) 
(declare-fun r () Real) 
(declare-fun v_shifted () Real) 
(declare-fun s () Real) 
(declare-fun t35uscore0dollarskuscore1_shifted () Real) 
(declare-fun vuscore2dollarskuscore29_shifted () Real) 
(declare-fun t () Real) 
(declare-fun ab () Real) 
(declare-fun u () Real) 
(declare-fun ac () Real) 
(assert (not 
(exists ((v Real)) (=> (xor (and (or (and (= j V (- f t)) (distinct (- y t) 0.0) (= (- y t) 2.0 (- d v_shifted)) (< (- (- x) (/
(* (- (- B))))) 0) (= (- Jlidu_new vuscore2dollarskuscore29_shifted) 2.0) (< (+ (/
 v2 )) (- ehbTa_new A_shifted)) (< 0.0 B)) (<= 0.0 (- HTSab_new (- b B)))) (<= (- HTSab_new (- 118 b B)) V) (<= 0.0 v2 V i) (< 0.0 V)) (< 0.0 (- CLPEA_new v_shifted))) (>= 0.0 (- a t)) (=> (xor (<= 0.0 v) (<= v (- a t))) (and (or (<= 0.0 j) (<= j V)) (<= 0.0 (+ (* (* (- 1.0) B) v) k) (+ (* (* (- 1.0) B) v) k) V) (<= (mod v 0.0) (- CLPEA_new v_shifted)))) (= (- ECxis_new ) 2.0))))) 
(assert (not 
(exists ((w Real)) (=> (and (or (and (xor (and (or ( and (and (=> (>= 0.0 r (/ 164 UAfuP_new v2)) (and (and (<= 0.0 (+ (* r)  I2 )) (<= (+ (* A_shifted r) (- I2)) s)) (<= r (- f n)))) (< 0.0 (- UAfuP_new v2))) (distinct z ab) (= u 1.0)) (<= 0.0 (- Jlidu_new I2))) (<= (* 230 Jlidu_new I2) s) (< z ab) (= q 2.0) (< z ac) (< 0.0 (- HTSab_new g)) (<= 0.0 (- d l))) (<= (- 30 d l) s)) (<= 0.0 A_shifted)) (< 0.0 s)) (< 0.0 (- f n))) (> (+ (* A_shifted (- UAfuP_new v2)) (- Jlidu_new I2)) s))))) 
(assert (= HTSab_new (+ g p))) 
(assert (= ECxis_new (+ h))) 
(assert (= a (+ t1428uscore0 t))) 
(assert (= b (mod B p))) 
(assert (= UAfuP_new (div v2 t35uscore0dollarskuscore1_shifted))) 
(assert (distinct c (+ k A_shifted))) 
(assert (= d (+ l v_shifted))) 
(assert (= Jlidu_new (+ I2 vuscore2dollarskuscore29_shifted))) 
(assert (distinct e (+ m t35uscore0dollarskuscore1_shifted))) 
(assert (= f (+ n t))) 
(assert (= y (div o t))) 
(assert (= CLPEA_new (div aa v_shifted))) 
(check-sat)

Z3 smt.arith.solver=6 throws out an assertion violation:

[650] % z3 smt.arith.solver=6 small.smt2
ASSERTION VIOLATION
File: ../src/smt/theory_lra.cpp
Line: 989
lp::tv::is_term(vi)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: b686bb6

[muchang]

Here is another simple case:

(set-option :rewriter.push_to_real false) 
(declare-fun a () Int) 
(declare-fun b () Int) 
(assert (> (+ (* (- a) (/ 6 b))) 9)) 
(check-sat)