A fuzzing framework for SMT solvers

Hi, When I used YinYang (fusion), I found it generated some instances contains syntax errors. For example:

(declare-fun scr1_liipp_0_c () Real)
(declare-fun scr1_liipp_0__main_offset () Real)
(declare-fun scr1_liipp_0__main_length () Real)
(declare-fun scr1_liipp_1_c () Real)
(declare-fun scr1_liipp_1__main_offset () Real)
(declare-fun scr1_liipp_1__main_length () Real)
(declare-fun scr1_liipp_2_c () Real)
(declare-fun scr1_liipp_2__main_offset () Real)
(declare-fun scr1_liipp_2__main_length () Real)
(declare-fun scr1_liipp_3_c () Real)
(declare-fun scr1_liipp_3__main_offset () Real)
(declare-fun scr1_liipp_3__main_length () Real)
(declare-fun scr1_liipp_4_replace_0 () Real)
(declare-fun scr1_liipp_4_replace_1 () Real)
(declare-fun scr1_liipp_5_replace_0 () Real)
(declare-fun scr1_liipp_5_replace_1 () Real)
(declare-fun scr1_motzkin_6304_0 () Real)
(declare-fun scr1_motzkin_6304_1 () Real)
(declare-fun scr1_motzkin_6304_2 () Real)
(declare-fun scr1_motzkin_6304_3 () Real)
(declare-fun scr1_motzkin_6304_4 () Real)
(declare-fun scr1_motzkin_6305_0 () Real)
(declare-fun scr1_motzkin_6305_1 () Real)
(declare-fun scr1_motzkin_6305_2 () Real)
(declare-fun scr1_motzkin_6305_3 () Real)
(declare-fun scr1_motzkin_6305_4 () Real)
(declare-fun scr1_motzkin_6306_0 () Real)
(declare-fun scr1_motzkin_6306_1 () Real)
(declare-fun scr1_motzkin_6306_2 () Real)
(declare-fun scr1_motzkin_6306_3 () Real)
(declare-fun scr1_motzkin_6307_0 () Real)
(declare-fun scr1_motzkin_6307_1 () Real)
(declare-fun scr1_motzkin_6307_2 () Real)
(declare-fun scr1_motzkin_6307_3 () Real)
(declare-fun scr1_motzkin_6308_0 () Real)
(declare-fun scr1_motzkin_6308_1 () Real)
(declare-fun scr1_motzkin_6308_2 () Real)
(declare-fun scr2_liipp_0_c () Real)
(declare-fun scr2_liipp_0__main_offset () Real)
(declare-fun scr2_liipp_0__main_length () Real)
(declare-fun scr2_liipp_1_c () Real)
(declare-fun scr2_liipp_1__main_offset () Real)
(declare-fun scr2_liipp_1__main_length () Real)
(declare-fun scr2_liipp_2_c () Real)
(declare-fun scr2_liipp_2__main_offset () Real)
(declare-fun scr2_liipp_2__main_length () Real)
(declare-fun scr2_liipp_3_c () Real)
(declare-fun scr2_liipp_3__main_offset () Real)
(declare-fun scr2_liipp_3__main_length () Real)
(declare-fun scr2_liipp_4_replace_0 () Real)
(declare-fun scr2_liipp_4_replace_1 () Real)
(declare-fun scr2_liipp_5_replace_0 () Real)
(declare-fun scr2_liipp_5_replace_1 () Real)
(declare-fun scr2_motzkin_6261_0 () Real)
(declare-fun scr2_motzkin_6261_1 () Real)
(declare-fun scr2_motzkin_6261_2 () Real)
(declare-fun scr2_motzkin_6261_3 () Real)
(declare-fun scr2_motzkin_6261_4 () Real)
(declare-fun scr2_motzkin_6262_0 () Real)
(declare-fun scr2_motzkin_6262_1 () Real)
(declare-fun scr2_motzkin_6262_2 () Real)
(declare-fun scr2_motzkin_6262_3 () Real)
(declare-fun scr2_motzkin_6262_4 () Real)
(declare-fun scr1_liipp_4_replace_0_scr2_motzkin_6263_1_fused () Real)
(declare-fun scr1_liipp_1__main_length_scr2_liipp_2_c_fused () Real)
(declare-fun scr1_liipp_2_c_scr2_liipp_2__main_offset_fused () Real)
(declare-fun scr1_motzkin_6307_3_scr2_liipp_4_replace_0_fused () Real)
(declare-fun scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused () Real)
(declare-fun scr1_liipp_2__main_length_scr2_liipp_0__main_offset_fused () Real)
(declare-fun scr1_liipp_1_c_scr2_motzkin_6262_3_fused () Real)
(declare-fun scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused () Real)
(declare-fun scr1_motzkin_6305_3_scr2_motzkin_6263_2_fused () Real)
(declare-fun scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused () Real)
(declare-fun scr1_liipp_0__main_offset_scr2_motzkin_6262_2_fused () Real)
(declare-fun scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused () Real)
(declare-fun scr1_motzkin_6307_2_scr2_motzkin_6264_0_fused () Real)
(declare-fun scr1_liipp_5_replace_1_scr2_motzkin_6263_0_fused () Real)
(declare-fun scr1_liipp_2__main_offset_scr2_liipp_0__main_length_fused () Real)
(declare-fun scr1_motzkin_6305_4_scr2_liipp_1_c_fused () Real)
(declare-fun scr1_liipp_3__main_offset_scr2_liipp_0_c_fused () Real)
(assert (and (and (and (>= scr1_motzkin_6304_0 0.0) (>= scr1_motzkin_6304_1 0.0) (>= scr1_motzkin_6304_2 0.0) (>= scr1_motzkin_6304_3 0.0) (>= scr1_motzkin_6304_4 0.0) (= (+ scr1_motzkin_6304_0 (* (- scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused scr2_motzkin_6261_1) (- 1.0)) (* scr1_motzkin_6304_4 (+ (* (- 1.0) (- scr1_liipp_0__main_offset_scr2_motzkin_6262_2_fused scr2_motzkin_6262_2)) 0.0))) 0.0) (= (+ scr1_motzkin_6304_2 (* scr1_motzkin_6304_3 (- 1.0)) (* scr1_motzkin_6304_4 (+ (* (- 1.0) scr1_liipp_0__main_length) 0.0))) 0.0) (<= (+ (* scr1_motzkin_6304_2 (- 40000.0)) (* scr1_motzkin_6304_3 40000.0) (* scr1_motzkin_6304_4 (+ (* (- 1.0) scr1_liipp_0_c) 0.0))) 0.0) (or (< (+ (* scr1_motzkin_6304_2 (- 40000.0)) (* scr1_motzkin_6304_3 40000.0) (* scr1_motzkin_6304_4 (+ (* (- 1.0) scr1_liipp_0_c) 0.0))) 0.0) (> 0.0 0.0)) (>= scr1_motzkin_6305_0 0.0) (>= scr1_motzkin_6305_1 0.0) (>= scr1_motzkin_6305_2 0.0) (>= scr1_motzkin_6305_3 0.0) (>= scr1_motzkin_6305_4 0.0) (= (+ scr1_motzkin_6305_0 (* scr1_motzkin_6305_1 (- 1.0)) (* scr1_motzkin_6305_4 (+ (* (- 1.0) scr1_liipp_1__main_offset) 0.0))) 0.0) (= (+ scr1_motzkin_6305_2 (* (- (- scr1_motzkin_6305_3_scr2_motzkin_6263_2_fused scr2_motzkin_6263_2) 350.94844) (- 1.0)) (* scr1_motzkin_6305_4 (+ (* (- 1.0) scr1_liipp_1__main_length) 0.0))) 0.0) (<= (+ (* scr1_motzkin_6305_2 (- 40000.0)) (* scr1_motzkin_6305_3 40000.0) (* scr1_motzkin_6305_4 (+ (* (- 1.0) (- (- scr1_liipp_1_c_scr2_motzkin_6262_3_fused 363.76579) scr2_motzkin_6262_3)) 0.0))) 0.0) (or (< (+ (* scr1_motzkin_6305_2 (- 40000.0)) (* scr1_motzkin_6305_3 40000.0)) 0.0) (> scr1_motzkin_6305_4 0.0))) (and (>= (- (- scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused scr2_liipp_1__main_offset) (- 922.62598)) 0.0) (>= scr1_motzkin_6306_1 0.0) (>= scr1_motzkin_6306_2 0.0) (>= scr1_motzkin_6306_3 0.0) (= (+ (* scr1_motzkin_6306_0 (- 1.0)) (* scr1_motzkin_6306_1 (+ (* (- 1.0) scr1_liipp_2__main_offset) 0.0)) (* scr1_motzkin_6306_2 (+ (* 1.0 (- scr1_liipp_0__main_offset_scr2_motzkin_6262_2_fused scr2_motzkin_6262_2)) 0.0)) (* scr1_motzkin_6306_3 (+ (* 1.0 scr1_liipp_1__main_offset) 0.0))) 0.0) (= (+ (- (- scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused scr2_liipp_1__main_offset) (- 922.62598)) (* scr1_motzkin_6306_1 (+ (* (- 1.0) scr1_liipp_2__main_length) 0.0)) (* scr1_motzkin_6306_2 (+ (* 1.0 scr1_liipp_0__main_length) 0.0)) (* scr1_motzkin_6306_3 (+ (* 1.0 scr1_liipp_1__main_length) 0.0))) 0.0) (<= (+ (* scr1_motzkin_6306_0 (- 1.0)) (* scr1_motzkin_6306_1 (+ (* (- 1.0) (- (- scr1_liipp_2_c_scr2_liipp_2__main_offset_fused scr2_liipp_2__main_offset) 829.94541)) 0.0)) (* scr1_motzkin_6306_2 (+ (* 1.0 scr1_liipp_0_c) 0.0)) (* scr1_motzkin_6306_3 (+ (* 1.0 (- (- scr1_liipp_1_c_scr2_motzkin_6262_3_fused 363.76579) scr2_motzkin_6262_3)) 0.0))) 0.0) (or (< (+ (* (- (- scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused scr2_liipp_1__main_offset) (- 922.62598)) (- 1.0)) (* scr1_motzkin_6306_1 (+ (* (- 1.0) scr1_liipp_2_c) 0.0)) (* scr1_motzkin_6306_3 (+ (* 1.0 scr1_liipp_1_c) 0.0))) 0.0) (> scr1_motzkin_6306_2 0.0)) (>= scr1_motzkin_6307_0 0.0) (>= (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr2_motzkin_6262_0) 0.0) (>= scr1_motzkin_6307_2 0.0) (>= scr1_motzkin_6307_3 0.0) (= (+ (* scr1_motzkin_6307_0 (- 1.0)) (* (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr2_motzkin_6262_0) (+ (* (- 1.0) (- (- scr1_liipp_3__main_offset_scr2_liipp_0_c_fused 243.32956) scr2_liipp_0_c)) 0.0)) (* scr1_motzkin_6307_2 (+ (* 1.0 scr1_liipp_0__main_offset) 0.0)) (* (- (- scr1_motzkin_6307_3_scr2_liipp_4_replace_0_fused 251.25255) scr2_liipp_4_replace_0) (+ (* 1.0 scr1_liipp_1__main_offset) 0.0))) 0.0) (= (+ scr1_motzkin_6307_0 (* (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr2_motzkin_6262_0) (+ (* (- 1.0) scr1_liipp_3__main_length) 0.0)) (* scr1_motzkin_6307_2 (+ (* 1.0 scr1_liipp_0__main_length) 0.0)) (* (- (- scr1_motzkin_6307_3_scr2_liipp_4_replace_0_fused 251.25255) scr2_liipp_4_replace_0) (+ (* 1.0 scr1_liipp_1__main_length) 0.0))) 0.0) (<= (+ (* scr1_motzkin_6307_0 (- 1.0)) (* (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr2_motzkin_6262_0) (+ (* (- 1.0) scr1_liipp_3_c) 0.0)) (* scr1_motzkin_6307_2 (+ (* 1.0 scr1_liipp_0_c) 0.0)) (* scr1_motzkin_6307_3 (+ (* 1.0 (- (- scr1_liipp_1_c_scr2_motzkin_6262_3_fused 363.76579) scr2_motzkin_6262_3)) 0.0))) 0.0) (or (< (+ (* scr1_motzkin_6307_0 (- 1.0)) (* (- (- scr1_motzkin_6307_3_scr2_liipp_4_replace_0_fused 251.25255) scr2_liipp_4_replace_0) (+ (* 1.0 scr1_liipp_1_c) 0.0))) 0.0) (> (+ (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr2_motzkin_6262_0) scr1_motzkin_6307_2) 0.0))) (and (>= scr1_motzkin_6308_0 0.0) (>= scr1_motzkin_6308_1 0.0) (>= scr1_motzkin_6308_2 0.0) (= (+ scr1_motzkin_6308_0 (* scr1_motzkin_6308_1 (+ (* 1.0 scr1_liipp_2__main_offset) 0.0)) (* scr1_motzkin_6308_2 (+ (* 1.0 (- (- scr1_liipp_3__main_offset_scr2_liipp_0_c_fused 243.32956) scr2_liipp_0_c)) 0.0))) 0.0) (= (+ (* scr1_motzkin_6308_0 (- 1.0)) (* scr1_motzkin_6308_1 (+ (* 1.0 (- (- scr1_liipp_2__main_length_scr2_liipp_0__main_offset_fused 428.59846) scr2_liipp_0__main_offset)) 0.0)) (* scr1_motzkin_6308_2 (+ (* 1.0 scr1_liipp_3__main_length) 0.0))) 0.0) (<= (+ (* scr1_motzkin_6308_0 3.0) (* scr1_motzkin_6308_1 (+ (* 1.0 (- (- scr1_liipp_2_c_scr2_liipp_2__main_offset_fused scr2_liipp_2__main_offset) 829.94541)) 0.0)) (* scr1_motzkin_6308_2 (+ (* 1.0 scr1_liipp_3_c) 0.0))) 0.0) (or (< (+ (* scr1_motzkin_6308_0 3.0) (* scr1_motzkin_6308_2 (+ (* 1.0 scr1_liipp_3_c) 0.0))) 0.0) (> scr1_motzkin_6308_1 0.0)))) (and (and (>= scr2_motzkin_6261_0 0.0) (>= (- scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused scr1_motzkin_6304_1) 0.0) (>= scr2_motzkin_6261_2 0.0) (>= scr2_motzkin_6261_3 0.0) (>= scr2_motzkin_6261_4 0.0) (= (+ (* scr2_motzkin_6261_0 (- 1.0)) (- scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused scr1_motzkin_6304_1) (* scr2_motzkin_6261_4 (+ (* (- 1.0) scr2_liipp_0__main_length) 0.0))) 0.0) (= (+ scr2_motzkin_6261_2 (* scr2_motzkin_6261_3 (- 1.0)) (* scr2_motzkin_6261_4 (+ (* (- 1.0) (- (- scr1_liipp_2__main_length_scr2_liipp_0__main_offset_fused 428.59846) scr1_liipp_2__main_length)) 0.0))) 0.0) (<= (+ (* scr2_motzkin_6261_0 1048.0) (* (- scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused scr1_motzkin_6304_1) (- 1048.0)) (* scr2_motzkin_6261_4 (+ (* (- 1.0) scr2_liipp_0_c) 0.0))) 0.0) (or (< (+ (* scr2_motzkin_6261_0 1048.0) (* (- scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused scr1_motzkin_6304_1) (- 1048.0)) (* scr2_motzkin_6261_4 (+ (* (- 1.0) scr2_liipp_0_c) 0.0))) 0.0) (> 0.0 0.0)) (>= (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr1_motzkin_6307_1) 0.0) (>= scr2_motzkin_6262_1 0.0) (>= scr2_motzkin_6262_2 0.0) (>= scr2_motzkin_6262_3 0.0) (>= (- (- scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused (- 232.60698)) scr1_liipp_4_replace_1) 0.0) (= (+ (* scr2_motzkin_6262_0 (- 1.0)) scr2_motzkin_6262_1 (* (- (- scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused (- 232.60698)) scr1_liipp_4_replace_1) (+ (* (- 1.0) scr2_liipp_1__main_length) 0.0))) 0.0) (= (+ scr2_motzkin_6262_2 (* scr2_motzkin_6262_3 (- 1.0)) (* (- (- scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused (- 232.60698)) scr1_liipp_4_replace_1) (+ (* (- 1.0) scr2_liipp_1__main_offset) 0.0))) 0.0) (<= (+ (* (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr1_motzkin_6307_1) 1048.0) (* scr2_motzkin_6262_1 (- 1048.0)) (* (- (- scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused (- 232.60698)) scr1_liipp_4_replace_1) (+ (* (- 1.0) scr2_liipp_1_c) 0.0))) 0.0) (or (< (+ (* scr2_motzkin_6262_0 1048.0) (* scr2_motzkin_6262_1 (- 1048.0))) 0.0) (> (- (- scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused (- 232.60698)) scr1_liipp_4_replace_1) 0.0))) (and (>= scr2_motzkin_6263_0 0.0) (>= scr2_motzkin_6263_1 0.0) (>= scr2_motzkin_6263_2 0.0) (>= scr2_motzkin_6263_3 0.0) (= (+ (* scr2_motzkin_6263_0 (- 1.0)) (* (- (- scr1_liipp_4_replace_0_scr2_motzkin_6263_1_fused 392.98169) scr1_liipp_4_replace_0) (+ (* (- 1.0) (- (- scr1_liipp_2_c_scr2_liipp_2__main_offset_fused scr1_liipp_2_c) 829.94541)) 0.0)) (* scr2_motzkin_6263_2 (+ (* 1.0 scr2_liipp_0__main_offset) 0.0)) (* scr2_motzkin_6263_3 (+ (* 1.0 (- (- scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused scr1_motzkin_6306_0) (- 922.62598))) 0.0))) 0.0) (= (+ scr2_motzkin_6263_0 (* (- (- scr1_liipp_4_replace_0_scr2_motzkin_6263_1_fused 392.98169) scr1_liipp_4_replace_0) (+ (* (- 1.0) scr2_liipp_2__main_length) 0.0)) (* (- (- scr1_motzkin_6305_3_scr2_motzkin_6263_2_fused scr1_motzkin_6305_3) 350.94844) (+ (* 1.0 (/ scr1_liipp_2__main_offset_scr2_liipp_0__main_length_fused scr1_liipp_2__main_offset)) 0.0)) (* scr2_motzkin_6263_3 (+ (* 1.0 scr2_liipp_1__main_length) 0.0))) 0.0) (<= (+ (* scr2_motzkin_6263_0 (- 1.0)) (* (- (- scr1_liipp_4_replace_0_scr2_motzkin_6263_1_fused 392.98169) scr1_liipp_4_replace_0) (+ (* (- 1.0) scr2_liipp_2_c) 0.0)) (* (- (- scr1_motzkin_6305_3_scr2_motzkin_6263_2_fused scr1_motzkin_6305_3) 350.94844) (+ (* 1.0 scr2_liipp_0_c) 0.0)) (* scr2_motzkin_6263_3 (+ (* 1.0 scr2_liipp_1_c) 0.0))) 0.0) (or (< (+ (* scr2_motzkin_6263_0 (- 1.0)) (* scr2_motzkin_6263_1 (+ (* (- 1.0) scr2_liipp_2_c) 0.0)) (* scr2_motzkin_6263_3 (+ (* 1.0 scr2_liipp_1_c) 0.0))) 0.0) (> (- (- scr1_motzkin_6305_3_scr2_motzkin_6263_2_fused scr1_motzkin_6305_3) 350.94844) 0.0)) (>= scr2_motzkin_6264_0 0.0) (>= scr2_motzkin_6264_1 0.0) (>= scr2_motzkin_6264_2 0.0) (>= scr2_motzkin_6264_3 0.0) (= (+ (* scr2_motzkin_6264_0 (- 1.0)) (* scr2_motzkin_6264_1 (+ (* (- 1.0) scr2_liipp_3__main_offset) 0.0)) (* scr2_motzkin_6264_2 (+ (* 1.0 scr2_liipp_0__main_offset) 0.0)) (* scr2_motzkin_6264_3 (+ (* 1.0 (- (- scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused scr1_motzkin_6306_0) (- 922.62598))) 0.0))) 0.0) (= (+ scr2_motzkin_6264_0 (* scr2_motzkin_6264_1 (+ (* (- 1.0) scr2_liipp_3__main_length) 0.0)) (* scr2_motzkin_6264_2 (+ (* 1.0 scr2_liipp_0__main_length) 0.0)) (* scr2_motzkin_6264_3 (+ (* 1.0 scr2_liipp_1__main_length) 0.0))) 0.0) (<= (+ (* scr2_motzkin_6264_0 (- 1.0)) (* scr2_motzkin_6264_1 (+ (* (- 1.0) scr2_liipp_3_c) 0.0)) (* scr2_motzkin_6264_2 (+ (* 1.0 scr2_liipp_0_c) 0.0)) (* scr2_motzkin_6264_3 (+ (* 1.0 scr2_liipp_1_c) 0.0))) 0.0) (or (< (+ (* scr2_motzkin_6264_0 (- 1.0)) (* scr2_motzkin_6264_3 (+ (* 1.0 (- (- scr1_motzkin_6305_4_scr2_liipp_1_c_fused scr1_motzkin_6305_4) (- 317.09221))) 0.0))) 0.0) (> (+ scr2_motzkin_6264_1 scr2_motzkin_6264_2) 0.0))) (and (>= scr2_motzkin_6265_0 0.0) (>= scr2_motzkin_6265_1 0.0) (>= scr2_motzkin_6265_2 0.0) (= (+ scr2_motzkin_6265_0 (* scr2_motzkin_6265_1 (+ (* 1.0 scr2_liipp_2__main_offset) 0.0)) (* scr2_motzkin_6265_2 (+ (* 1.0 scr2_liipp_3__main_offset) 0.0))) 0.0) (= (+ (* scr2_motzkin_6265_0 (- 1.0)) (* scr2_motzkin_6265_1 (+ (* 1.0 scr2_liipp_2__main_length) 0.0)) (* scr2_motzkin_6265_2 (+ (* 1.0 scr2_liipp_3__main_length) 0.0))) 0.0) (<= (+ (* scr2_motzkin_6265_0 3.0) (* scr2_motzkin_6265_1 (+ (* 1.0 scr2_liipp_2_c) 0.0)) (* scr2_motzkin_6265_2 (+ (* 1.0 scr2_liipp_3_c) 0.0))) 0.0) (or (< (+ (* scr2_motzkin_6265_0 3.0) (* scr2_motzkin_6265_2 (+ (* 1.0 scr2_liipp_3_c) 0.0))) 0.0) (> scr2_motzkin_6265_1 0.0))))))
(declare-fun scr2_motzkin_6263_0 () Real)
(declare-fun scr2_motzkin_6263_1 () Real)
(declare-fun scr2_motzkin_6263_2 () Real)
(declare-fun scr2_motzkin_6263_3 () Real)
(declare-fun scr2_motzkin_6264_0 () Real)
(declare-fun scr2_motzkin_6264_1 () Real)
(declare-fun scr2_motzkin_6264_2 () Real)
(declare-fun scr2_motzkin_6264_3 () Real)
(declare-fun scr2_motzkin_6265_0 () Real)
(declare-fun scr2_motzkin_6265_1 () Real)
(declare-fun scr2_motzkin_6265_2 () Real)
(check-sat)

For this instance, z3 returns

(error "line 81 column 1192: unknown constant scr2_motzkin_6263_2")
sat

Commit: 5b821b0

Together with Lucas Weitzendorf, I am working at a fusion functions generator for our AST project.

Our generator can build very long funsion functions and their inversions and we would like to allow multiple constants to appear within the same block. This PR allow such specifications (see below for the format description) and is retro compatible.

I rely here on the naming convention (constant names are in the format c[0-9]*) as I have seen this is already practically used now.

The new proposed format is:

#begin
<declaration of x>
<declaration of y>
<declaration of z>
[<declaration of c_i>*]
<assert fusion function>
<assert inversion function>
<assert inversion function>
# end

Add the command line option --keep-seeds (-k) with default value True. When set to False, scratch files will not be kept in the scratch folder after the Fuzzer executes, but the files will be created anyway.

Add command line option for Semantic Fusion to generate fusion functions with the fusion function generator: https://github.com/nicdard/fusion-function-generator/pull/78 Use --generate-functions option (int value, the size of the functions) to generate a fusion function on demand to perform the fuse step of semantic fusion.

The current version of yinyang only uses the last processed seed in the name of the bug log. This is not ideal if multiple seeds are used to trigger the bug, such as in semantic fusion.

Experiments on larger formulas, e.g., QF_FP 40kB+ formulas with highly nested expressions exposed hotspots while parsing.

Actions:

• Identify SMT-LIB formulas on which the parser times out
• Profiling
• Fix the hotspots

Consider the following output

Summary:
Passed time: 48821s
Generated mutants: 1346751
Used seeds: 6
Crash issues: 0
Unsound issues: 0
Timeout cases: 0
Ignored issues: 139924

A common questions (asked by students) seem to be: "What are Ignored Issues?".

Actions:

• (possibly) change the wording
• add a description about

Actions:

• make src/args.py consistent with the description in the documentation
• prettify the output for yinyang.py (called without args) and help and yinyang.py --help

$ python3.9 yinyang.py 
usage: yinyang.py [-h] [-s {opfuzz,fusion}] [-o {sat,unsat}] [-i ITERATIONS] [-m MODULO] [-t TIMEOUT] [-d] [-optfuzz OPTFUZZ]
                  [-name NAME] [-bugs BUGSFOLDER] [-scratch SCRATCHFOLDER] [-opconfig OPCONFIG] [-fusionfun FUSIONFUN] [-km]
                  SOLVER_CLIS PATH_TO_SEEDS [PATH_TO_SEEDS ...]
yinyang.py: error: the following arguments are required: SOLVER_CLIS, PATH_TO_SEEDS

confuses more than it helps (with all the optional options etc)

$ python3.9 yinyang.py --help
usage: yinyang.py [-h] [-s {opfuzz,fusion}] [-o {sat,unsat}] [-i ITERATIONS] [-m MODULO] [-t TIMEOUT] [-d] [-optfuzz OPTFUZZ]
                  [-name NAME] [-bugs BUGSFOLDER] [-scratch SCRATCHFOLDER] [-opconfig OPCONFIG] [-fusionfun FUSIONFUN] [-km]
                  SOLVER_CLIS PATH_TO_SEEDS [PATH_TO_SEEDS ...]

positional arguments:
  SOLVER_CLIS           solvers' command-line interfaces for solving .smt2 files
  PATH_TO_SEEDS         path to the seed files/folders

optional arguments:
  -h, --help            show this help message and exit
  -s {opfuzz,fusion}, --strategy {opfuzz,fusion}
                        set fuzzing strategy
  -o {sat,unsat}, --oracle {sat,unsat}
                        set oracle for semantic fusion strategy (default: unknown)
  -i ITERATIONS, --iterations ITERATIONS
                        set mutating iterations for each seed/pair (default: 300 for Type-Aware Operator Mutation, 30 for
                        SemanticFusion)
  -m MODULO, --modulo MODULO
                        determines when the mutant will be forwarded to the solvers for opfuzz
  -t TIMEOUT, --timeout TIMEOUT
                        set timeout for solving process (default: 8)
  -d, --diagnose        forward solver outputs to stdout e.g. for solver cli diagnosis
  -optfuzz OPTFUZZ, --optfuzz OPTFUZZ
                        read solvers' option setting and enable option fuzzing
  -name NAME, --name NAME
                        set name of this fuzzing instance (default: random string)
  -bugs BUGSFOLDER, --bugsfolder BUGSFOLDER
                        set bug folder (default: /Users/windomin/repositories/yinyang_private/bugs)
  -scratch SCRATCHFOLDER, --scratchfolder SCRATCHFOLDER
                        set scratch folder (default: /Users/windomin/repositories/yinyang_private/scratch)
  -opconfig OPCONFIG, --opconfig OPCONFIG
                        set operator mutation configuration (default:
                        /Users/windomin/repositories/yinyang_private/config/operator_mutations.txt)
  -fusionfun FUSIONFUN, --fusionfun FUSIONFUN
                        set fusion function configuration (default:
                        /Users/windomin/repositories/yinyang_private/config/fusion_functions.txt)
  -km, --keep-mutants   Do not delete the mutants generated in the scratchfolder.

could also be better, with the explanation text more to the right.

Issue with quantifiers of the form (forall ((t1 String) (t2 String)) expr in which case t2 would be considered free variable leading to an unsoundness in unsat fusion.

Add the command line option --keep-seeds (-k) with default value True. When set to False, scratch files will not be kept in the scratch folder after the Fuzzer executes, but the files will be created anyway.

I did some major changes on the handling of compound types, e.g. (Array (Array X Y) Y). As far as I understand, in the current code:

1. The raw parser produces a structured representation of them, e.g. the grammar has all the necessary rules.
2. The AstVisitor converts this structure into textual representation
3. The sort2type function converts sort strings back to type objects ( ARRAY_TYPE, BITVECTOR_TYPE, etc.).

I propose to eliminate sort2type entirely and produce structured type representations in the AstVisitor directly, as done in this PR. This is only halfway done though, as BitVector and FloatingPoint is still parsed in sort2type.

Apart from that it looks like Opfuzz uses sort2type for constructing rules, so if that is needed then we could move sort2type into the opfuzz module.

Added support BVUGT, BVUGE, BVSGE, BVSLE. I tested a bit ad-hoc with:

#!/usr/bin/env bash
for f in path-to-semantic-fusion-seeds/BV/sat/*.smt2; do
  cp $f tests/unit/test.smt2;
  python -m unittest -k large tests/RunUnitTests.py;
done
git checkout tests/unit/test.smt2

and they all pass, same for BV/unsat/. I did not wait for QF_BV to finish, but the first few hundred worked fine.

Greetings,

While trying to parse code written in smtlibv2 through yinyang, I found some bugs that yinyang cannot parse some codes.

For example, parsing results of yinyang are (None, None) about the below codes.

Could I know why it happened?

Thanks for your time!

(set-info :smt-lib-version 2.6) (set-logic QF_ABV) (set-info :source | Crafted benchmarks created for "Sharing is Caring: Combination of Theories" by Dejan Jovanovic and Clark Barrett. In Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS '11), Oct. 2011, pp. 195-210. Based on Example 4 from Section 5. |) (set-info :category "crafted") (set-info :status sat) (declare-fun a_0 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_0 () (_ BitVec 128)) (declare-fun a_1 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_1 () (_ BitVec 128)) (declare-fun a_2 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_2 () (_ BitVec 128)) (declare-fun a_3 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_3 () (_ BitVec 128)) (declare-fun a_4 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_4 () (_ BitVec 128)) (declare-fun a_5 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_5 () (_ BitVec 128)) (declare-fun a_6 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_6 () (_ BitVec 128)) (declare-fun a_7 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_7 () (_ BitVec 128)) (declare-fun a_8 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_8 () (_ BitVec 128)) (declare-fun a_9 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_9 () (_ BitVec 128)) (declare-fun a_10 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_10 () (_ BitVec 128)) (declare-fun a_11 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_11 () (_ BitVec 128)) (declare-fun a_12 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_12 () (_ BitVec 128)) (declare-fun a_13 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_13 () (_ BitVec 128)) (declare-fun a_14 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_14 () (_ BitVec 128)) (declare-fun a_15 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_15 () (_ BitVec 128)) (declare-fun a_16 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_16 () (_ BitVec 128)) (declare-fun a_17 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_17 () (_ BitVec 128)) (declare-fun a_18 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_18 () (_ BitVec 128)) (declare-fun a_19 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_19 () (_ BitVec 128)) (declare-fun a_20 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_20 () (_ BitVec 128)) (declare-fun a_21 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_21 () (_ BitVec 128)) (declare-fun a_22 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_22 () (_ BitVec 128)) (declare-fun a_23 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_23 () (_ BitVec 128)) (declare-fun a_24 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_24 () (_ BitVec 128)) (declare-fun a_25 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_25 () (_ BitVec 128)) (declare-fun a_26 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_26 () (_ BitVec 128)) (declare-fun a_27 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_27 () (_ BitVec 128)) (declare-fun a_28 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_28 () (_ BitVec 128)) (declare-fun a_29 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_29 () (_ BitVec 128)) (declare-fun a_30 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_30 () (_ BitVec 128)) (declare-fun a_31 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_31 () (_ BitVec 128)) (declare-fun a_32 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_32 () (_ BitVec 128)) (declare-fun a_33 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_33 () (_ BitVec 128)) (declare-fun a_34 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_34 () (_ BitVec 128)) (declare-fun a_35 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_35 () (_ BitVec 128)) (declare-fun a_36 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_36 () (_ BitVec 128)) (declare-fun a_37 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_37 () (_ BitVec 128)) (declare-fun a_38 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_38 () (_ BitVec 128)) (declare-fun a_39 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_39 () (_ BitVec 128)) (declare-fun a_40 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_40 () (_ BitVec 128)) (declare-fun a_41 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_41 () (_ BitVec 128)) (declare-fun a_42 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_42 () (_ BitVec 128)) (declare-fun a_43 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_43 () (_ BitVec 128)) (declare-fun a_44 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_44 () (_ BitVec 128)) (declare-fun a_45 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_45 () (_ BitVec 128)) (declare-fun a_46 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_46 () (_ BitVec 128)) (declare-fun a_47 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_47 () (_ BitVec 128)) (declare-fun a_48 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_48 () (_ BitVec 128)) (declare-fun a_49 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_49 () (_ BitVec 128)) (assert (not (= (select a_0 (bvmul x_0 x_1)) (select a_1 (bvmul x_1 x_2))))) (assert (not (= (select a_1 (bvmul x_1 x_2)) (select a_2 (bvmul x_2 x_3))))) (assert (not (= (select a_2 (bvmul x_2 x_3)) (select a_3 (bvmul x_3 x_4))))) (assert (not (= (select a_3 (bvmul x_3 x_4)) (select a_4 (bvmul x_4 x_5))))) (assert (not (= (select a_4 (bvmul x_4 x_5)) (select a_5 (bvmul x_5 x_6))))) (assert (not (= (select a_5 (bvmul x_5 x_6)) (select a_6 (bvmul x_6 x_7))))) (assert (not (= (select a_6 (bvmul x_6 x_7)) (select a_7 (bvmul x_7 x_8))))) (assert (not (= (select a_7 (bvmul x_7 x_8)) (select a_8 (bvmul x_8 x_9))))) (assert (not (= (select a_8 (bvmul x_8 x_9)) (select a_9 (bvmul x_9 x_10))))) (assert (not (= (select a_9 (bvmul x_9 x_10)) (select a_10 (bvmul x_10 x_11))))) (assert (not (= (select a_10 (bvmul x_10 x_11)) (select a_11 (bvmul x_11 x_12))))) (assert (not (= (select a_11 (bvmul x_11 x_12)) (select a_12 (bvmul x_12 x_13))))) (assert (not (= (select a_12 (bvmul x_12 x_13)) (select a_13 (bvmul x_13 x_14))))) (assert (not (= (select a_13 (bvmul x_13 x_14)) (select a_14 (bvmul x_14 x_15))))) (assert (not (= (select a_14 (bvmul x_14 x_15)) (select a_15 (bvmul x_15 x_16))))) (assert (not (= (select a_15 (bvmul x_15 x_16)) (select a_16 (bvmul x_16 x_17))))) (assert (not (= (select a_16 (bvmul x_16 x_17)) (select a_17 (bvmul x_17 x_18))))) (assert (not (= (select a_17 (bvmul x_17 x_18)) (select a_18 (bvmul x_18 x_19))))) (assert (not (= (select a_18 (bvmul x_18 x_19)) (select a_19 (bvmul x_19 x_20))))) (assert (not (= (select a_19 (bvmul x_19 x_20)) (select a_20 (bvmul x_20 x_21))))) (assert (not (= (select a_20 (bvmul x_20 x_21)) (select a_21 (bvmul x_21 x_22))))) (assert (not (= (select a_21 (bvmul x_21 x_22)) (select a_22 (bvmul x_22 x_23))))) (assert (not (= (select a_22 (bvmul x_22 x_23)) (select a_23 (bvmul x_23 x_24))))) (assert (not (= (select a_23 (bvmul x_23 x_24)) (select a_24 (bvmul x_24 x_25))))) (assert (not (= (select a_24 (bvmul x_24 x_25)) (select a_25 (bvmul x_25 x_26))))) (assert (not (= (select a_25 (bvmul x_25 x_26)) (select a_26 (bvmul x_26 x_27))))) (assert (not (= (select a_26 (bvmul x_26 x_27)) (select a_27 (bvmul x_27 x_28))))) (assert (not (= (select a_27 (bvmul x_27 x_28)) (select a_28 (bvmul x_28 x_29))))) (assert (not (= (select a_28 (bvmul x_28 x_29)) (select a_29 (bvmul x_29 x_30))))) (assert (not (= (select a_29 (bvmul x_29 x_30)) (select a_30 (bvmul x_30 x_31))))) (assert (not (= (select a_30 (bvmul x_30 x_31)) (select a_31 (bvmul x_31 x_32))))) (assert (not (= (select a_31 (bvmul x_31 x_32)) (select a_32 (bvmul x_32 x_33))))) (assert (not (= (select a_32 (bvmul x_32 x_33)) (select a_33 (bvmul x_33 x_34))))) (assert (not (= (select a_33 (bvmul x_33 x_34)) (select a_34 (bvmul x_34 x_35))))) (assert (not (= (select a_34 (bvmul x_34 x_35)) (select a_35 (bvmul x_35 x_36))))) (assert (not (= (select a_35 (bvmul x_35 x_36)) (select a_36 (bvmul x_36 x_37))))) (assert (not (= (select a_36 (bvmul x_36 x_37)) (select a_37 (bvmul x_37 x_38))))) (assert (not (= (select a_37 (bvmul x_37 x_38)) (select a_38 (bvmul x_38 x_39))))) (assert (not (= (select a_38 (bvmul x_38 x_39)) (select a_39 (bvmul x_39 x_40))))) (assert (not (= (select a_39 (bvmul x_39 x_40)) (select a_40 (bvmul x_40 x_41))))) (assert (not (= (select a_40 (bvmul x_40 x_41)) (select a_41 (bvmul x_41 x_42))))) (assert (not (= (select a_41 (bvmul x_41 x_42)) (select a_42 (bvmul x_42 x_43))))) (assert (not (= (select a_42 (bvmul x_42 x_43)) (select a_43 (bvmul x_43 x_44))))) (assert (not (= (select a_43 (bvmul x_43 x_44)) (select a_44 (bvmul x_44 x_45))))) (assert (not (= (select a_44 (bvmul x_44 x_45)) (select a_45 (bvmul x_45 x_46))))) (assert (not (= (select a_45 (bvmul x_45 x_46)) (select a_46 (bvmul x_46 x_47))))) (assert (not (= (select a_46 (bvmul x_46 x_47)) (select a_47 (bvmul x_47 x_48))))) (assert (not (= (select a_47 (bvmul x_47 x_48)) (select a_48 (bvmul x_48 x_49))))) (assert (not (= (select a_48 (bvmul x_48 x_49)) (select a_49 (bvmul x_49 x_0))))) (assert (not (= (select a_49 (bvmul x_49 x_0)) (select a_0 (bvmul x_0 x_1))))) (check-sat) (exit)

yinyang (version 0.3.0 installed via pip) consumes ~40G of memory when running with the provided semantic-fusion-seeds/QF_SLIA seeds. Using more seeds will increase memory consumption (with the QF_SLIA logic from SMT-LIB yinyang runs out of memory on my machine with 128G memory). The memory consumption increases rapidly on startup and seems to be stable after yinyang actually starts fuzzing. The same behavior can be observed with the current git version on master.

The command I use to run yinyang is: yinyang ./solver.sh semantic-fusion-seeds/QF_SLIA/

This makes the typechecker fail (but z3 and cvc4 are happy with it):

(declare-fun x () Int)
(assert (=>
	(= x 3)
	(forall ((x Int)) (let ((?y x))
		(= ?y 3)
	))
))
(check-sat)

The output is:

src.parsing.typechecker.TypeCheckError: Ill-typed expression 
term:           (= x 3)
faulty subterm: 3
expected:       Unknown
actual:         Int

The error disappears when the quantified and global variable have different names.