ins

counterexample.dump.ia32_Mul_base_disp--Add32.load32.Mul32.Mulh_u32.0005.smt2

@@ -0,0 +1,291 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_BV)
+(set-info :source |
+Generated by: Sebastian Buchwald, Andreas Fried
+Generated on: 2017-04-27
+Generator: Instruction Selection Synthesis
+Application: Synthesize x86 mul instruction from Intermediate Representation
+Target solver: Z3
+Publications: https://publikationen.bibliothek.kit.edu/1000066092
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun c-0-loc () (_ BitVec 5))
+(declare-fun c-0-in-0-loc () (_ BitVec 5))
+(declare-fun c-0-in-1-loc () (_ BitVec 5))
+(declare-fun c-1-loc () (_ BitVec 5))
+(declare-fun c-1-in-0-loc () (_ BitVec 5))
+(declare-fun c-1-in-1-loc () (_ BitVec 5))
+(declare-fun c-3-loc () (_ BitVec 5))
+(declare-fun c-3-in-0-loc () (_ BitVec 5))
+(declare-fun c-3-in-1-loc () (_ BitVec 5))
+(declare-fun c-4-loc () (_ BitVec 5))
+(declare-fun c-4-in-0-loc () (_ BitVec 5))
+(declare-fun c-4-in-1-loc () (_ BitVec 5))
+(declare-fun result-0-loc () (_ BitVec 5))
+(declare-fun result-1-loc () (_ BitVec 5))
+(declare-fun result-2-loc () (_ BitVec 5))
+(declare-fun arg-1 () (_ BitVec 32))
+(declare-fun arg-0 () (_ BitVec 32))
+(declare-fun arg-2 () (_ BitVec 36))
+(declare-fun arg-3 () (_ BitVec 32))
+(declare-fun symbolic-goal-result-2 () (_ BitVec 32))
+(declare-fun symbolic-goal-result-1 () (_ BitVec 36))
+(declare-fun symbolic-goal-result-0 () (_ BitVec 32))
+(declare-fun symbolic-c-4-out-0 () (_ BitVec 32))
+(declare-fun symbolic-c-0-in-0 () (_ BitVec 32))
+(declare-fun symbolic-c-3-out-0 () (_ BitVec 32))
+(declare-fun symbolic-c-1-out-1 () (_ BitVec 32))
+(declare-fun symbolic-c-0-out-0 () (_ BitVec 32))
+(declare-fun symbolic-c-0-in-1 () (_ BitVec 32))
+(declare-fun symbolic-c-1-out-0 () (_ BitVec 36))
+(declare-fun symbolic-c-1-in-0 () (_ BitVec 36))
+(declare-fun symbolic-c-1-in-1 () (_ BitVec 32))
+(declare-fun symbolic-c-3-in-0 () (_ BitVec 32))
+(declare-fun symbolic-c-3-in-1 () (_ BitVec 32))
+(declare-fun symbolic-c-4-in-0 () (_ BitVec 32))
+(declare-fun symbolic-c-4-in-1 () (_ BitVec 32))
+(declare-fun symbolic-ir-result-0 () (_ BitVec 32))
+(declare-fun symbolic-ir-result-1 () (_ BitVec 36))
+(declare-fun symbolic-ir-result-2 () (_ BitVec 32))
+(assert
+ (= c-0-loc (_ bv4 5)))
+(assert
+ (= c-0-in-0-loc (_ bv1 5)))
+(assert
+ (= c-0-in-1-loc (_ bv0 5)))
+(assert
+ (= c-1-loc (_ bv5 5)))
+(assert
+ (= c-1-in-0-loc (_ bv2 5)))
+(assert
+ (= c-1-in-1-loc (_ bv4 5)))
+(assert
+ (= c-3-loc (_ bv8 5)))
+(assert
+ (= c-3-in-0-loc (_ bv6 5)))
+(assert
+ (= c-3-in-1-loc (_ bv3 5)))
+(assert
+ (= c-4-loc (_ bv7 5)))
+(assert
+ (= c-4-in-0-loc (_ bv3 5)))
+(assert
+ (= c-4-in-1-loc (_ bv6 5)))
+(assert
+ (= result-0-loc (_ bv8 5)))
+(assert
+ (= result-1-loc (_ bv5 5)))
+(assert
+ (= result-2-loc (_ bv7 5)))
+(assert
+ (let ((?x67250 (bvadd (bvadd arg-0 (bvmul (_ bv0 32) (_ bv1 32))) arg-1)))
+ (let ((?x98001 (bvadd ?x67250 (_ bv3 32))))
+ (let (($x22238 (= ?x98001 ?x98001)))
+ (let ((?x78435 (bvadd ?x67250 (_ bv2 32))))
+ (let (($x37725 (= ?x98001 ?x78435)))
+ (let (($x19584 (or (or (or false (= ?x98001 ?x67250)) (= ?x98001 (bvadd ?x67250 (_ bv1 32)))) $x37725)))
+ (let (($x117920 (= ?x78435 ?x98001)))
+ (let (($x84656 (= ?x78435 ?x78435)))
+ (let (($x7391 (or (or (or false (= ?x78435 ?x67250)) (= ?x78435 (bvadd ?x67250 (_ bv1 32)))) $x84656)))
+ (let ((?x122387 (bvadd ?x67250 (_ bv1 32))))
+ (let (($x120825 (= ?x122387 ?x98001)))
+ (let (($x93865 (or (or (or (or false (= ?x122387 ?x67250)) (= ?x122387 ?x122387)) (= ?x122387 ?x78435)) $x120825)))
+ (let (($x32432 (= ?x67250 ?x98001)))
+ (let (($x11639 (or (or (or (or false (= ?x67250 ?x67250)) (= ?x67250 ?x122387)) (= ?x67250 ?x78435)) $x32432)))
+ (and (and (and (and true $x11639) $x93865) (or $x7391 $x117920)) (or $x19584 $x22238)))))))))))))))))
+(assert
+ (let ((?x67250 (bvadd (bvadd arg-0 (bvmul (_ bv0 32) (_ bv1 32))) arg-1)))
+ (let (($x75209 (= ?x67250 ?x67250)))
+ (let ((?x122387 (bvadd ?x67250 (_ bv1 32))))
+ (let (($x15946 (= ?x67250 ?x122387)))
+ (let ((?x78435 (bvadd ?x67250 (_ bv2 32))))
+ (let (($x104283 (= ?x67250 ?x78435)))
+ (let ((?x136424 (ite $x104283 ((_ extract 25 18) arg-2) (ite $x15946 ((_ extract 16 9) arg-2) (ite $x75209 ((_ extract 7 0) arg-2) (_ bv85 8))))))
+ (let ((?x98001 (bvadd ?x67250 (_ bv3 32))))
+ (let (($x32432 (= ?x67250 ?x98001)))
+ (let ((?x91014 ((_ rotate_left 26) (_ bv1 36))))
+ (let ((?x61780 (ite $x104283 ?x91014 (ite $x15946 ((_ rotate_left 17) (_ bv1 36)) (ite $x75209 ((_ rotate_left 8) (_ bv1 36)) (_ bv0 36))))))
+ (let ((?x89763 ((_ rotate_left 35) (_ bv1 36))))
+ (let ((?x55705 (bvor arg-2 (ite $x32432 ?x89763 ?x61780))))
+ (let (($x56855 (= ?x122387 ?x67250)))
+ (let (($x37249 (= ?x122387 ?x122387)))
+ (let (($x97809 (= ?x122387 ?x78435)))
+ (let ((?x148079 (ite $x97809 ((_ extract 25 18) ?x55705) (ite $x37249 ((_ extract 16 9) ?x55705) (ite $x56855 ((_ extract 7 0) ?x55705) (_ bv85 8))))))
+ (let (($x120825 (= ?x122387 ?x98001)))
+ (let ((?x76583 (ite $x97809 ?x91014 (ite $x37249 ((_ rotate_left 17) (_ bv1 36)) (ite $x56855 ((_ rotate_left 8) (_ bv1 36)) (_ bv0 36))))))
+ (let ((?x14108 (bvor ?x55705 (ite $x120825 ?x89763 ?x76583))))
+ (let (($x35995 (= ?x78435 ?x67250)))
+ (let (($x90073 (= ?x78435 ?x122387)))
+ (let (($x84656 (= ?x78435 ?x78435)))
+ (let ((?x77410 (ite $x84656 ((_ extract 25 18) ?x14108) (ite $x90073 ((_ extract 16 9) ?x14108) (ite $x35995 ((_ extract 7 0) ?x14108) (_ bv85 8))))))
+ (let (($x117920 (= ?x78435 ?x98001)))
+ (let ((?x61876 (ite $x84656 ?x91014 (ite $x90073 ((_ rotate_left 17) (_ bv1 36)) (ite $x35995 ((_ rotate_left 8) (_ bv1 36)) (_ bv0 36))))))
+ (let ((?x158755 (bvor ?x14108 (ite $x117920 ?x89763 ?x61876))))
+ (let (($x129590 (= ?x98001 ?x67250)))
+ (let (($x140218 (= ?x98001 ?x122387)))
+ (let (($x37725 (= ?x98001 ?x78435)))
+ (let ((?x25078 (ite $x37725 ((_ extract 25 18) ?x158755) (ite $x140218 ((_ extract 16 9) ?x158755) (ite $x129590 ((_ extract 7 0) ?x158755) (_ bv85 8))))))
+ (let (($x22238 (= ?x98001 ?x98001)))
+ (let ((?x107013 (concat (concat (ite $x22238 ((_ extract 34 27) ?x158755) ?x25078) (ite $x117920 ((_ extract 34 27) ?x14108) ?x77410)) (ite $x120825 ((_ extract 34 27) ?x55705) ?x148079))))
+ (let ((?x51700 (bvmul (concat (_ bv0 32) arg-3) (concat (_ bv0 32) (concat ?x107013 (ite $x32432 ((_ extract 34 27) arg-2) ?x136424))))))
+ (let ((?x67178 (ite $x37725 ?x91014 (ite $x140218 ((_ rotate_left 17) (_ bv1 36)) (ite $x129590 ((_ rotate_left 8) (_ bv1 36)) (_ bv0 36))))))
+ (let (($x128246 (and (and true (= symbolic-goal-result-0 ((_ extract 31 0) ?x51700))) (= symbolic-goal-result-1 (bvor ?x158755 (ite $x22238 ?x89763 ?x67178))))))
+ (and $x128246 (= symbolic-goal-result-2 ((_ extract 63 32) ?x51700))))))))))))))))))))))))))))))))))))))))
+(assert
+ (let (($x86076 (=> (= c-0-in-0-loc (bvadd c-4-loc (_ bv0 5))) (= symbolic-c-0-in-0 symbolic-c-4-out-0))))
+ (let (($x131287 (=> (= c-0-in-0-loc (bvadd c-3-loc (_ bv0 5))) (= symbolic-c-0-in-0 symbolic-c-3-out-0))))
+ (let (($x102541 (=> (= c-0-in-0-loc (bvadd c-1-loc (_ bv1 5))) (= symbolic-c-0-in-0 symbolic-c-1-out-1))))
+ (let (($x47343 (=> (= c-0-in-0-loc (bvadd c-0-loc (_ bv0 5))) (= symbolic-c-0-in-0 symbolic-c-0-out-0))))
+ (let (($x86507 (and true (=> (= c-0-in-0-loc (_ bv0 5)) (= symbolic-c-0-in-0 arg-0)))))
+ (let (($x106160 (and (and $x86507 (=> (= c-0-in-0-loc (_ bv1 5)) (= symbolic-c-0-in-0 arg-1))) (=> (= c-0-in-0-loc (_ bv3 5)) (= symbolic-c-0-in-0 arg-3)))))
+ (and (and (and (and $x106160 $x47343) $x102541) $x131287) $x86076))))))))
+(assert
+ (let (($x144182 (=> (= c-0-in-1-loc (bvadd c-4-loc (_ bv0 5))) (= symbolic-c-0-in-1 symbolic-c-4-out-0))))
+ (let (($x76342 (=> (= c-0-in-1-loc (bvadd c-3-loc (_ bv0 5))) (= symbolic-c-0-in-1 symbolic-c-3-out-0))))
+ (let (($x31395 (=> (= c-0-in-1-loc (bvadd c-1-loc (_ bv1 5))) (= symbolic-c-0-in-1 symbolic-c-1-out-1))))
+ (let (($x104552 (=> (= c-0-in-1-loc (bvadd c-0-loc (_ bv0 5))) (= symbolic-c-0-in-1 symbolic-c-0-out-0))))
+ (let (($x13544 (and true (=> (= c-0-in-1-loc (_ bv0 5)) (= symbolic-c-0-in-1 arg-0)))))
+ (let (($x40637 (and (and $x13544 (=> (= c-0-in-1-loc (_ bv1 5)) (= symbolic-c-0-in-1 arg-1))) (=> (= c-0-in-1-loc (_ bv3 5)) (= symbolic-c-0-in-1 arg-3)))))
+ (and (and (and (and $x40637 $x104552) $x31395) $x76342) $x144182))))))))
+(assert
+ (and true (= symbolic-c-0-out-0 (bvadd symbolic-c-0-in-0 symbolic-c-0-in-1))))
+(assert
+ (let (($x15090 (=> (= c-1-in-0-loc (bvadd c-1-loc (_ bv0 5))) (= symbolic-c-1-in-0 symbolic-c-1-out-0))))
+ (let (($x37880 (and true (=> (= c-1-in-0-loc (_ bv2 5)) (= symbolic-c-1-in-0 arg-2)))))
+ (and $x37880 $x15090))))
+(assert
+ (let (($x156682 (=> (= c-1-in-1-loc (bvadd c-4-loc (_ bv0 5))) (= symbolic-c-1-in-1 symbolic-c-4-out-0))))
+ (let (($x154735 (=> (= c-1-in-1-loc (bvadd c-3-loc (_ bv0 5))) (= symbolic-c-1-in-1 symbolic-c-3-out-0))))
+ (let (($x121402 (=> (= c-1-in-1-loc (bvadd c-1-loc (_ bv1 5))) (= symbolic-c-1-in-1 symbolic-c-1-out-1))))
+ (let (($x2075 (=> (= c-1-in-1-loc (bvadd c-0-loc (_ bv0 5))) (= symbolic-c-1-in-1 symbolic-c-0-out-0))))
+ (let (($x22599 (and true (=> (= c-1-in-1-loc (_ bv0 5)) (= symbolic-c-1-in-1 arg-0)))))
+ (let (($x108608 (and (and $x22599 (=> (= c-1-in-1-loc (_ bv1 5)) (= symbolic-c-1-in-1 arg-1))) (=> (= c-1-in-1-loc (_ bv3 5)) (= symbolic-c-1-in-1 arg-3)))))
+ (and (and (and (and $x108608 $x2075) $x121402) $x154735) $x156682))))))))
+(assert
+ (let ((?x67250 (bvadd (bvadd arg-0 (bvmul (_ bv0 32) (_ bv1 32))) arg-1)))
+ (let (($x126418 (= symbolic-c-1-in-1 ?x67250)))
+ (let ((?x122387 (bvadd ?x67250 (_ bv1 32))))
+ (let (($x1008 (= symbolic-c-1-in-1 ?x122387)))
+ (let ((?x138190 (ite $x1008 ((_ extract 16 9) symbolic-c-1-in-0) (ite $x126418 ((_ extract 7 0) symbolic-c-1-in-0) (_ bv85 8)))))
+ (let ((?x78435 (bvadd ?x67250 (_ bv2 32))))
+ (let (($x40084 (= symbolic-c-1-in-1 ?x78435)))
+ (let ((?x98001 (bvadd ?x67250 (_ bv3 32))))
+ (let (($x30045 (= symbolic-c-1-in-1 ?x98001)))
+ (let ((?x34576 (ite $x30045 ((_ extract 34 27) symbolic-c-1-in-0) (ite $x40084 ((_ extract 25 18) symbolic-c-1-in-0) ?x138190))))
+ (let ((?x91014 ((_ rotate_left 26) (_ bv1 36))))
+ (let ((?x119788 (ite $x40084 ?x91014 (ite $x1008 ((_ rotate_left 17) (_ bv1 36)) (ite $x126418 ((_ rotate_left 8) (_ bv1 36)) (_ bv0 36))))))
+ (let ((?x89763 ((_ rotate_left 35) (_ bv1 36))))
+ (let ((?x79127 (bvor symbolic-c-1-in-0 (ite $x30045 ?x89763 ?x119788))))
+ (let ((?x145723 (bvadd symbolic-c-1-in-1 (_ bv1 32))))
+ (let (($x117957 (= ?x145723 ?x67250)))
+ (let (($x65166 (= ?x145723 ?x122387)))
+ (let (($x113245 (= ?x145723 ?x78435)))
+ (let ((?x56226 (ite $x113245 ((_ extract 25 18) ?x79127) (ite $x65166 ((_ extract 16 9) ?x79127) (ite $x117957 ((_ extract 7 0) ?x79127) (_ bv85 8))))))
+ (let (($x56779 (= ?x145723 ?x98001)))
+ (let ((?x124685 (ite $x113245 ?x91014 (ite $x65166 ((_ rotate_left 17) (_ bv1 36)) (ite $x117957 ((_ rotate_left 8) (_ bv1 36)) (_ bv0 36))))))
+ (let ((?x99668 (bvor ?x79127 (ite $x56779 ?x89763 ?x124685))))
+ (let ((?x20853 (bvadd symbolic-c-1-in-1 (_ bv2 32))))
+ (let (($x133609 (= ?x20853 ?x67250)))
+ (let (($x27883 (= ?x20853 ?x122387)))
+ (let (($x9097 (= ?x20853 ?x78435)))
+ (let ((?x26942 (ite $x9097 ((_ extract 25 18) ?x99668) (ite $x27883 ((_ extract 16 9) ?x99668) (ite $x133609 ((_ extract 7 0) ?x99668) (_ bv85 8))))))
+ (let (($x37959 (= ?x20853 ?x98001)))
+ (let ((?x113168 (ite $x9097 ?x91014 (ite $x27883 ((_ rotate_left 17) (_ bv1 36)) (ite $x133609 ((_ rotate_left 8) (_ bv1 36)) (_ bv0 36))))))
+ (let ((?x104721 (bvor ?x99668 (ite $x37959 ?x89763 ?x113168))))
+ (let ((?x14214 (bvadd symbolic-c-1-in-1 (_ bv3 32))))
+ (let (($x30631 (= ?x14214 ?x67250)))
+ (let (($x10220 (= ?x14214 ?x122387)))
+ (let (($x112517 (= ?x14214 ?x78435)))
+ (let ((?x63357 (ite $x112517 ((_ extract 25 18) ?x104721) (ite $x10220 ((_ extract 16 9) ?x104721) (ite $x30631 ((_ extract 7 0) ?x104721) (_ bv85 8))))))
+ (let (($x44701 (= ?x14214 ?x98001)))
+ (let ((?x146751 (concat (concat (ite $x44701 ((_ extract 34 27) ?x104721) ?x63357) (ite $x37959 ((_ extract 34 27) ?x99668) ?x26942)) (ite $x56779 ((_ extract 34 27) ?x79127) ?x56226))))
+ (let ((?x17901 (ite $x112517 ?x91014 (ite $x10220 ((_ rotate_left 17) (_ bv1 36)) (ite $x30631 ((_ rotate_left 8) (_ bv1 36)) (_ bv0 36))))))
+ (and (and true (= symbolic-c-1-out-0 (bvor ?x104721 (ite $x44701 ?x89763 ?x17901)))) (= symbolic-c-1-out-1 (concat ?x146751 ?x34576))))))))))))))))))))))))))))))))))))))))))
+(assert
+ (let (($x109695 (=> (= c-3-in-0-loc (bvadd c-4-loc (_ bv0 5))) (= symbolic-c-3-in-0 symbolic-c-4-out-0))))
+ (let (($x51104 (=> (= c-3-in-0-loc (bvadd c-3-loc (_ bv0 5))) (= symbolic-c-3-in-0 symbolic-c-3-out-0))))
+ (let (($x49273 (=> (= c-3-in-0-loc (bvadd c-1-loc (_ bv1 5))) (= symbolic-c-3-in-0 symbolic-c-1-out-1))))
+ (let (($x24527 (=> (= c-3-in-0-loc (bvadd c-0-loc (_ bv0 5))) (= symbolic-c-3-in-0 symbolic-c-0-out-0))))
+ (let (($x87850 (and true (=> (= c-3-in-0-loc (_ bv0 5)) (= symbolic-c-3-in-0 arg-0)))))
+ (let (($x76222 (and (and $x87850 (=> (= c-3-in-0-loc (_ bv1 5)) (= symbolic-c-3-in-0 arg-1))) (=> (= c-3-in-0-loc (_ bv3 5)) (= symbolic-c-3-in-0 arg-3)))))
+ (and (and (and (and $x76222 $x24527) $x49273) $x51104) $x109695))))))))
+(assert
+ (let (($x32280 (=> (= c-3-in-1-loc (bvadd c-4-loc (_ bv0 5))) (= symbolic-c-3-in-1 symbolic-c-4-out-0))))
+ (let (($x77045 (=> (= c-3-in-1-loc (bvadd c-3-loc (_ bv0 5))) (= symbolic-c-3-in-1 symbolic-c-3-out-0))))
+ (let (($x78308 (=> (= c-3-in-1-loc (bvadd c-1-loc (_ bv1 5))) (= symbolic-c-3-in-1 symbolic-c-1-out-1))))
+ (let (($x40941 (=> (= c-3-in-1-loc (bvadd c-0-loc (_ bv0 5))) (= symbolic-c-3-in-1 symbolic-c-0-out-0))))
+ (let (($x63408 (and true (=> (= c-3-in-1-loc (_ bv0 5)) (= symbolic-c-3-in-1 arg-0)))))
+ (let (($x150250 (and (and $x63408 (=> (= c-3-in-1-loc (_ bv1 5)) (= symbolic-c-3-in-1 arg-1))) (=> (= c-3-in-1-loc (_ bv3 5)) (= symbolic-c-3-in-1 arg-3)))))
+ (and (and (and (and $x150250 $x40941) $x78308) $x77045) $x32280))))))))
+(assert
+ (and true (= symbolic-c-3-out-0 (bvmul symbolic-c-3-in-0 symbolic-c-3-in-1))))
+(assert
+ (let (($x63457 (=> (= c-4-in-0-loc (bvadd c-4-loc (_ bv0 5))) (= symbolic-c-4-in-0 symbolic-c-4-out-0))))
+ (let (($x71864 (=> (= c-4-in-0-loc (bvadd c-3-loc (_ bv0 5))) (= symbolic-c-4-in-0 symbolic-c-3-out-0))))
+ (let (($x99615 (=> (= c-4-in-0-loc (bvadd c-1-loc (_ bv1 5))) (= symbolic-c-4-in-0 symbolic-c-1-out-1))))
+ (let (($x48078 (=> (= c-4-in-0-loc (bvadd c-0-loc (_ bv0 5))) (= symbolic-c-4-in-0 symbolic-c-0-out-0))))
+ (let (($x59339 (and true (=> (= c-4-in-0-loc (_ bv0 5)) (= symbolic-c-4-in-0 arg-0)))))
+ (let (($x46178 (and (and $x59339 (=> (= c-4-in-0-loc (_ bv1 5)) (= symbolic-c-4-in-0 arg-1))) (=> (= c-4-in-0-loc (_ bv3 5)) (= symbolic-c-4-in-0 arg-3)))))
+ (and (and (and (and $x46178 $x48078) $x99615) $x71864) $x63457))))))))
+(assert
+ (let (($x132203 (=> (= c-4-in-1-loc (bvadd c-4-loc (_ bv0 5))) (= symbolic-c-4-in-1 symbolic-c-4-out-0))))
+ (let (($x124059 (=> (= c-4-in-1-loc (bvadd c-3-loc (_ bv0 5))) (= symbolic-c-4-in-1 symbolic-c-3-out-0))))
+ (let (($x43986 (=> (= c-4-in-1-loc (bvadd c-1-loc (_ bv1 5))) (= symbolic-c-4-in-1 symbolic-c-1-out-1))))
+ (let (($x47565 (=> (= c-4-in-1-loc (bvadd c-0-loc (_ bv0 5))) (= symbolic-c-4-in-1 symbolic-c-0-out-0))))
+ (let (($x147809 (and true (=> (= c-4-in-1-loc (_ bv0 5)) (= symbolic-c-4-in-1 arg-0)))))
+ (let (($x101263 (and (and $x147809 (=> (= c-4-in-1-loc (_ bv1 5)) (= symbolic-c-4-in-1 arg-1))) (=> (= c-4-in-1-loc (_ bv3 5)) (= symbolic-c-4-in-1 arg-3)))))
+ (and (and (and (and $x101263 $x47565) $x43986) $x124059) $x132203))))))))
+(assert
+ (let ((?x100613 ((_ extract 63 32) (bvmul ((_ zero_extend 64) symbolic-c-4-in-0) ((_ zero_extend 64) symbolic-c-4-in-1)))))
+ (and true (= symbolic-c-4-out-0 ?x100613))))
+(assert
+ (let (($x79605 (=> (= result-0-loc (bvadd c-4-loc (_ bv0 5))) (= symbolic-ir-result-0 symbolic-c-4-out-0))))
+ (let (($x62994 (=> (= result-0-loc (bvadd c-3-loc (_ bv0 5))) (= symbolic-ir-result-0 symbolic-c-3-out-0))))
+ (let (($x57390 (=> (= result-0-loc (bvadd c-1-loc (_ bv1 5))) (= symbolic-ir-result-0 symbolic-c-1-out-1))))
+ (let (($x20208 (=> (= result-0-loc (bvadd c-0-loc (_ bv0 5))) (= symbolic-ir-result-0 symbolic-c-0-out-0))))
+ (let (($x94249 (and true (=> (= result-0-loc (_ bv0 5)) (= symbolic-ir-result-0 arg-0)))))
+ (let (($x104401 (and $x94249 (=> (= result-0-loc (_ bv1 5)) (= symbolic-ir-result-0 arg-1)))))
+ (let (($x59974 (and $x104401 (=> (= result-0-loc (_ bv3 5)) (= symbolic-ir-result-0 arg-3)))))
+ (and (and (and (and $x59974 $x20208) $x57390) $x62994) $x79605)))))))))
+(assert
+ (let (($x98259 (=> (= result-1-loc (bvadd c-1-loc (_ bv0 5))) (= symbolic-ir-result-1 symbolic-c-1-out-0))))
+ (let (($x87305 (and true (=> (= result-1-loc (_ bv2 5)) (= symbolic-ir-result-1 arg-2)))))
+ (and $x87305 $x98259))))
+(assert
+ (let (($x65925 (=> (= result-2-loc (bvadd c-4-loc (_ bv0 5))) (= symbolic-ir-result-2 symbolic-c-4-out-0))))
+ (let (($x110045 (=> (= result-2-loc (bvadd c-3-loc (_ bv0 5))) (= symbolic-ir-result-2 symbolic-c-3-out-0))))
+ (let (($x54176 (=> (= result-2-loc (bvadd c-1-loc (_ bv1 5))) (= symbolic-ir-result-2 symbolic-c-1-out-1))))
+ (let (($x2889 (=> (= result-2-loc (bvadd c-0-loc (_ bv0 5))) (= symbolic-ir-result-2 symbolic-c-0-out-0))))
+ (let (($x23019 (and true (=> (= result-2-loc (_ bv0 5)) (= symbolic-ir-result-2 arg-0)))))
+ (let (($x25602 (and $x23019 (=> (= result-2-loc (_ bv1 5)) (= symbolic-ir-result-2 arg-1)))))
+ (let (($x16832 (and $x25602 (=> (= result-2-loc (_ bv3 5)) (= symbolic-ir-result-2 arg-3)))))
+ (and (and (and (and $x16832 $x2889) $x54176) $x110045) $x65925)))))))))
+(assert
+ (let ((?x67250 (bvadd (bvadd arg-0 (bvmul (_ bv0 32) (_ bv1 32))) arg-1)))
+(let ((?x98001 (bvadd ?x67250 (_ bv3 32))))
+(let ((?x14214 (bvadd symbolic-c-1-in-1 (_ bv3 32))))
+(let (($x44701 (= ?x14214 ?x98001)))
+(let ((?x78435 (bvadd ?x67250 (_ bv2 32))))
+(let (($x112517 (= ?x14214 ?x78435)))
+(let (($x55802 (or (or (or false (= ?x14214 ?x67250)) (= ?x14214 (bvadd ?x67250 (_ bv1 32)))) $x112517)))
+(let ((?x20853 (bvadd symbolic-c-1-in-1 (_ bv2 32))))
+(let (($x37959 (= ?x20853 ?x98001)))
+(let (($x9097 (= ?x20853 ?x78435)))
+(let (($x51767 (or (or (or false (= ?x20853 ?x67250)) (= ?x20853 (bvadd ?x67250 (_ bv1 32)))) $x9097)))
+(let ((?x145723 (bvadd symbolic-c-1-in-1 (_ bv1 32))))
+(let (($x56779 (= ?x145723 ?x98001)))
+(let (($x113245 (= ?x145723 ?x78435)))
+(let (($x76487 (or (or (or false (= ?x145723 ?x67250)) (= ?x145723 (bvadd ?x67250 (_ bv1 32)))) $x113245)))
+(let (($x30045 (= symbolic-c-1-in-1 ?x98001)))
+(let (($x40084 (= symbolic-c-1-in-1 ?x78435)))
+(let ((?x122387 (bvadd ?x67250 (_ bv1 32))))
+(let (($x1008 (= symbolic-c-1-in-1 ?x122387)))
+(let (($x35129 (or (or (or (or false (= symbolic-c-1-in-1 ?x67250)) $x1008) $x40084) $x30045)))
+(let (($x59983 (and (and (and (and true $x35129) (or $x76487 $x56779)) (or $x51767 $x37959)) (or $x55802 $x44701))))
+(let (($x86822 (and (and (and (and (and true true) $x59983) true) true) (= symbolic-ir-result-0 symbolic-goal-result-0))))
+(let (($x47515 (and (and $x86822 (= symbolic-ir-result-1 symbolic-goal-result-1)) (= symbolic-ir-result-2 symbolic-goal-result-2))))
+(not $x47515)))))))))))))))))))))))))
+(check-sat)
+(exit)