(set-info :source |printed by MathSAT|)
(declare-fun PRED13 () Bool)
(declare-fun PRED0 () Bool)
(declare-fun PRED34 () Bool)
(declare-fun |g::__cil_tmp3@3| () (_ BitVec 32))
(declare-fun |g::i@4| () (_ BitVec 32))
(declare-fun PRED17 () Bool)
(declare-fun PRED26 () Bool)
(declare-fun PRED22 () Bool)
(declare-fun PRED23 () Bool)
(declare-fun PRED24 () Bool)
(declare-fun |g::__cil_tmp4@3| () (_ BitVec 32))
(declare-fun |main::b@3| () (_ BitVec 32))
(declare-fun PRED32 () Bool)
(declare-fun PRED25 () Bool)
(declare-fun PRED16 () Bool)
(declare-fun PRED5 () Bool)
(declare-fun *int@5 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun pstate () (_ BitVec 32))
(declare-fun |*(void)*@5| ((_ BitVec 32)) (_ BitVec 32))
(declare-fun pp () (_ BitVec 32))
(declare-fun *int@6 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun PRED33 () Bool)
(declare-fun |g::pointer@2| () (_ BitVec 32))
(declare-fun |g::i@3| () (_ BitVec 32))
(define-fun .def_7321 () (_ BitVec 32) (bvadd (_ bv1 32) |g::i@4|))
(define-fun .def_7322 () (_ BitVec 32) (bvshl .def_7321 (_ bv2 32)))
(define-fun .def_7323 () (_ BitVec 32) (bvadd pp .def_7322))
(define-fun .def_7325 () (_ BitVec 32) (|*(void)*@5| .def_7323))
(define-fun .def_10270 () Bool (= |main::b@3| .def_7325))
(define-fun .def_10274 () Bool (= PRED32 .def_10270))
(define-fun .def_2006 () (_ BitVec 32) (bvshl |g::i@4| (_ bv2 32)))
(define-fun .def_2069 () (_ BitVec 32) (bvadd pp .def_2006))
(define-fun .def_2070 () (_ BitVec 32) (|*(void)*@5| .def_2069))
(define-fun .def_9984 () Bool (= |main::b@3| .def_2070))
(define-fun .def_10272 () Bool (= .def_9984 PRED33))
(define-fun .def_1008 () (_ BitVec 32) (|*(void)*@5| pp))
(define-fun .def_9987 () Bool (= |main::b@3| .def_1008))
(define-fun .def_10173 () Bool (= .def_9987 PRED34))
(define-fun .def_7699 () Bool (= |g::i@4| (_ bv0 32)))
(define-fun .def_7704 () Bool (= PRED24 .def_7699))
(define-fun .def_7633 () Bool (= |g::i@4| (_ bv1 32)))
(define-fun .def_7702 () Bool (= .def_7633 PRED25))
(define-fun .def_7698 () Bool (= |g::i@4| (_ bv2 32)))
(define-fun .def_7700 () Bool (= PRED26 .def_7698))
(define-fun .def_7326 () (_ BitVec 32) (bvmul (_ bv4294967295 32) .def_7325))
(define-fun .def_7327 () (_ BitVec 32) (bvadd |g::pointer@2| .def_7326))
(define-fun .def_7328 () Bool (= .def_7327 (_ bv4294967295 32)))
(define-fun .def_7331 () Bool (= PRED22 .def_7328))
(define-fun .def_5378 () Bool (= |g::pointer@2| .def_2070))
(define-fun .def_7329 () Bool (= .def_5378 PRED23))
(define-fun .def_1241 () (_ BitVec 32) (*int@6 pstate))
(define-fun .def_1846 () Bool (= .def_1241 (_ bv1 32)))
(define-fun .def_5308 () Bool (= .def_1846 PRED13))
(define-fun .def_5305 () Bool (= .def_2006 (_ bv0 32)))
(define-fun .def_5306 () Bool (= PRED16 .def_5305))
(define-fun .def_2007 () (_ BitVec 32) (bvadd pstate .def_2006))
(define-fun .def_2009 () (_ BitVec 32) (*int@6 .def_2007))
(define-fun .def_2010 () Bool (= .def_2009 (_ bv1 32)))
(define-fun .def_2011 () (_ BitVec 32) (ite .def_2010 (_ bv1 32) (_ bv0 32)))
(define-fun .def_2012 () Bool (= .def_2011 (_ bv0 32)))
(define-fun .def_2014 () Bool (= PRED0 .def_2012))
(define-fun .def_2013 () Bool (= PRED5 .def_2010))
(define-fun .def_2015 () Bool (and .def_2013 .def_2014))
(define-fun .def_5307 () Bool (and .def_2015 .def_5306))
(define-fun .def_5309 () Bool (and .def_5307 .def_5308))
(define-fun .def_2706 () Bool (= |g::pointer@2| .def_1008))
(define-fun .def_5261 () Bool (= .def_2706 PRED17))
(define-fun .def_5310 () Bool (and .def_5261 .def_5309))
(define-fun .def_7330 () Bool (and .def_5310 .def_7329))
(define-fun .def_7332 () Bool (and .def_7330 .def_7331))
(define-fun .def_7701 () Bool (and .def_7332 .def_7700))
(define-fun .def_7703 () Bool (and .def_7701 .def_7702))
(define-fun .def_7705 () Bool (and .def_7703 .def_7704))
(define-fun .def_10271 () Bool (and .def_7705 .def_10173))
(define-fun .def_10273 () Bool (and .def_10271 .def_10272))
(define-fun .def_10275 () Bool (and .def_10273 .def_10274))
(define-fun .def_381 () (_ BitVec 32) (bvshl |g::i@3| (_ bv2 32)))
(define-fun .def_382 () (_ BitVec 32) (bvadd pp .def_381))
(define-fun .def_1615 () (_ BitVec 32) (|*(void)*@5| .def_382))
(define-fun .def_10172 () Bool (= |main::b@3| .def_1615))
(define-fun .def_10227 () Bool (not .def_10172))
(define-fun .def_9988 () Bool (not .def_9987))
(define-fun .def_10228 () Bool (and .def_9988 .def_10227))
(define-fun .def_2000 () (_ BitVec 32) (bvadd (_ bv1 32) |g::i@3|))
(define-fun .def_2017 () (_ BitVec 32) (bvshl .def_2000 (_ bv2 32)))
(define-fun .def_5373 () (_ BitVec 32) (bvadd pp .def_2017))
(define-fun .def_5374 () (_ BitVec 32) (|*(void)*@5| .def_5373))
(define-fun .def_9981 () Bool (= |main::b@3| .def_5374))
(define-fun .def_10229 () Bool (and .def_9981 .def_10228))
(define-fun .def_7641 () Bool (= |g::i@3| (_ bv2 32)))
(define-fun .def_7668 () Bool (not .def_7641))
(define-fun .def_10230 () Bool (and .def_7668 .def_10229))
(define-fun .def_7642 () Bool (= |g::i@3| (_ bv1 32)))
(define-fun .def_7667 () Bool (not .def_7642))
(define-fun .def_10231 () Bool (and .def_7667 .def_10230))
(define-fun .def_371 () Bool (= |g::i@3| (_ bv0 32)))
(define-fun .def_10232 () Bool (and .def_371 .def_10231))
(define-fun .def_7229 () Bool (= |g::pointer@2| .def_1615))
(define-fun .def_10233 () Bool (and .def_7229 .def_10232))
(define-fun .def_5375 () (_ BitVec 32) (bvmul (_ bv4294967295 32) .def_5374))
(define-fun .def_5376 () (_ BitVec 32) (bvadd |g::pointer@2| .def_5375))
(define-fun .def_5377 () Bool (= .def_5376 (_ bv4294967295 32)))
(define-fun .def_10234 () Bool (and .def_5377 .def_10233))
(define-fun .def_10235 () Bool (and .def_2706 .def_10234))
(define-fun .def_1992 () Bool (= .def_381 (_ bv0 32)))
(define-fun .def_10236 () Bool (and .def_1992 .def_10235))
(define-fun .def_1018 () (_ BitVec 32) (*int@5 pstate))
(define-fun .def_1597 () Bool (= .def_1018 (_ bv1 32)))
(define-fun .def_10237 () Bool (and .def_1597 .def_10236))
(define-fun .def_395 () (_ BitVec 32) (bvadd pstate .def_381))
(define-fun .def_1591 () (_ BitVec 32) (*int@5 .def_395))
(define-fun .def_1592 () Bool (= .def_1591 (_ bv1 32)))
(define-fun .def_10238 () Bool (and .def_1592 .def_10237))
(define-fun .def_1593 () (_ BitVec 32) (ite .def_1592 (_ bv1 32) (_ bv0 32)))
(define-fun .def_1594 () Bool (= .def_1593 (_ bv0 32)))
(define-fun .def_1621 () Bool (not .def_1594))
(define-fun .def_10239 () Bool (and .def_1621 .def_10238))
(define-fun .def_2002 () Bool (= .def_2000 |g::i@4|))
(define-fun .def_1616 () Bool (= |g::__cil_tmp4@3| .def_1615))
(define-fun .def_379 () Bool (= |g::pointer@2| |g::__cil_tmp3@3|))
(define-fun .def_1617 () Bool (and .def_379 .def_1616))
(define-fun .def_373 () Bool (bvslt |g::i@3| (_ bv2 32)))
(define-fun .def_374 () (_ BitVec 32) (ite .def_373 (_ bv1 32) (_ bv0 32)))
(define-fun .def_375 () Bool (= .def_374 (_ bv0 32)))
(define-fun .def_376 () Bool (not .def_375))
(define-fun .def_1618 () Bool (and .def_376 .def_1617))
(define-fun .def_389 () Bool (= |g::__cil_tmp3@3| |g::__cil_tmp4@3|))
(define-fun .def_390 () (_ BitVec 32) (ite .def_389 (_ bv1 32) (_ bv0 32)))
(define-fun .def_391 () Bool (= .def_390 (_ bv0 32)))
(define-fun .def_1620 () Bool (and .def_391 .def_1618))
(define-fun .def_1242 () Bool (= .def_1018 .def_1241))
(define-fun .def_20 () (_ BitVec 32) (bvadd (_ bv4 32) pstate))
(define-fun .def_1236 () (_ BitVec 32) (*int@6 .def_20))
(define-fun .def_1014 () (_ BitVec 32) (*int@5 .def_20))
(define-fun .def_1237 () Bool (= .def_1014 .def_1236))
(define-fun .def_1454 () Bool (and .def_1237 .def_1242))
(define-fun .def_1997 () Bool (and .def_1454 .def_1620))
(define-fun .def_1993 () Bool (or .def_1242 .def_1992))
(define-fun .def_1989 () Bool (= .def_381 (_ bv4 32)))
(define-fun .def_1990 () Bool (or .def_1237 .def_1989))
(define-fun .def_1994 () Bool (and .def_1990 .def_1993))
(define-fun .def_1840 () (_ BitVec 32) (*int@6 .def_395))
(define-fun .def_1987 () Bool (= .def_1840 (_ bv2 32)))
(define-fun .def_1995 () Bool (and .def_1987 .def_1994))
(define-fun .def_392 () Bool (not .def_391))
(define-fun .def_1619 () Bool (and .def_392 .def_1618))
(define-fun .def_1622 () Bool (and .def_1619 .def_1621))
(define-fun .def_1996 () Bool (and .def_1622 .def_1995))
(define-fun .def_1998 () Bool (or .def_1996 .def_1997))
(define-fun .def_2003 () Bool (and .def_1998 .def_2002))
(define-fun .def_23 () (_ BitVec 32) (bvadd (_ bv8 32) pp))
(define-fun .def_26 () Bool (bvslt pstate .def_23))
(define-fun .def_27 () Bool (not .def_26))
(define-fun .def_24 () Bool (bvslt (_ bv0 32) .def_23))
(define-fun .def_28 () Bool (and .def_24 .def_27))
(define-fun .def_15 () Bool (bvslt (_ bv0 32) pp))
(define-fun .def_29 () Bool (and .def_15 .def_28))
(define-fun .def_2004 () Bool (and .def_29 .def_2003))
(define-fun .def_10269 () Bool (and .def_2004 .def_10239))
(define-fun .def_10276 () Bool (and .def_10269 .def_10275))
(assert .def_10276)
(check-allsat (PRED13 PRED16 PRED17 PRED22 PRED26 PRED32))