;; MathSAT API call trace
;; generated on So 02 Nov 2025 14:01:38 CET
(set-option :global-declarations true)
(set-option :config "verbosity=0")
(set-option :config "proof_generation=false")
(set-option :config "interpolation=false")
(set-option :config "model_generation=false")
(set-option :config "bool_model_generation=false")
(set-option :config "unsat_core_generation=0")
(set-option :config "random_seed=42")
(set-option :config "debug.dump_theory_lemmas=false")
(set-option :config "debug.solver_enabled=true")
(set-option :config "printer.bv_number_format=0")
(set-option :config "printer.fp_number_format=1")
(set-option :config "printer.defines_prefix=")
(set-option :config "printer.model_as_formula=false")
(set-option :config "preprocessor.toplevel_propagation=true")
(set-option :config "preprocessor.toplevel_propagation_limit=0")
(set-option :config "preprocessor.simplification=55")
(set-option :config "preprocessor.ite_minimization=false")
(set-option :config "preprocessor.ite_minimization_call_limit=150000")
(set-option :config "preprocessor.interpolation_ite_elimination=false")
(set-option :config "preprocessor.partial_nnf_conversion=false")
(set-option :config "preprocessor.full_cnf_conversion=false")
(set-option :config "dpll.restart_strategy=0")
(set-option :config "dpll.restart_initial=200")
(set-option :config "dpll.restart_geometric_factor=1.5")
(set-option :config "dpll.store_tlemmas=false")
(set-option :config "dpll.branching_random_frequency=0.001")
(set-option :config "dpll.branching_initial_phase=0")
(set-option :config "dpll.branching_cache_phase=2")
(set-option :config "dpll.branching_random_invalidate_phase_cache=false")
(set-option :config "dpll.branching_random_ignore_polarity=true")
(set-option :config "dpll.ghost_filtering=true")
(set-option :config "dpll.minimize_model=false")
(set-option :config "dpll.allsat_minimize_model=false")
(set-option :config "dpll.allsat_allow_duplicates=false")
(set-option :config "dpll.pop_btpoint_reset_var_order=true")
(set-option :config "dpll.glucose_var_activity=false")
(set-option :config "dpll.glucose_learnt_minimization=false")
(set-option :config "dpll.interpolation_mode=0")
(set-option :config "dpll.proof_simplification=false")
(set-option :config "dpll.preprocessor.mode=0")
(set-option :config "dpll.preprocessor.clause_size_limit=20")
(set-option :config "dpll.preprocessor.subsumption_size_limit=1000")
(set-option :config "dpll.preprocessor.elimination_grow_limit=0")
(set-option :config "dpll.preprocessor.elimination_phase=1")
(set-option :config "dpll.preprocessor.elimination_recent_vars_only=false")
(set-option :config "dpll.preprocessor.try_reelimination=true")
(set-option :config "theory.eq_propagation=true")
(set-option :config "theory.interface_eq_policy=2")
(set-option :config "theory.pairwise_interface_eq=true")
(set-option :config "theory.interface_eq_batch_size=100")
(set-option :config "theory.pure_literal_filtering=false")
(set-option :config "theory.euf.enabled=true")
(set-option :config "theory.euf.dyn_ack=0")
(set-option :config "theory.euf.dyn_ack_threshold=1")
(set-option :config "theory.euf.dyn_ack_limit=1000")
(set-option :config "theory.la.enabled=true")
(set-option :config "theory.la.split_rat_eq=false")
(set-option :config "theory.la.delay_alien=false")
(set-option :config "theory.la.pivoting_greedy_threshold=0")
(set-option :config "theory.la.lazy_expl_threshold=10")
(set-option :config "theory.la.interpolation_laz_use_floor=true")
(set-option :config "theory.la.pure_equality_filtering=true")
(set-option :config "theory.la.detect_euf_fragment=false")
(set-option :config "theory.la.deduction_enabled=true")
(set-option :config "theory.la.laz_equality_elimination=true")
(set-option :config "theory.la.laz_internal_branch_and_bound=true")
(set-option :config "theory.la.laz_internal_branch_and_bound_limit=1")
(set-option :config "theory.la.laz_cuts_from_proofs_mode=3")
(set-option :config "theory.la.laz_enabled=true")
(set-option :config "theory.la.laz_unit_cube_test=true")
(set-option :config "theory.la.interpolation_mode=0")
(set-option :config "theory.bv.enabled=true")
(set-option :config "theory.bv.div_by_zero_mode=0")
(set-option :config "theory.bv.delay_propagated_eqs=true")
(set-option :config "theory.bv.eager=true")
(set-option :config "theory.bv.bit_blast_mode=1")
(set-option :config "theory.bv.interpolation_mode=0")
(set-option :config "theory.bv.proof_simplification=false")
(set-option :config "theory.bv.lazydpll.restart_strategy=0")
(set-option :config "theory.bv.lazydpll.restart_initial=200")
(set-option :config "theory.bv.lazydpll.restart_geometric_factor=1.5")
(set-option :config "theory.bv.lazydpll.branching_random_frequency=0")
(set-option :config "theory.bv.lazydpll.branching_initial_phase=0")
(set-option :config "theory.bv.lazydpll.branching_cache_phase=2")
(set-option :config "theory.bv.lazydpll.branching_random_invalidate_phase_cache=false")
(set-option :config "theory.bv.lazydpll.branching_random_ignore_polarity=true")
(set-option :config "theory.bv.lazydpll.ghost_filtering=false")
(set-option :config "theory.bv.lazydpll.glucose_var_activity=false")
(set-option :config "theory.bv.lazydpll.glucose_learnt_minimization=false")
(set-option :config "theory.arr.enabled=true")
(set-option :config "theory.arr.mode=0")
(set-option :config "theory.arr.lazy_lemmas=false")
(set-option :config "theory.arr.max_ext_lemmas=0")
(set-option :config "theory.arr.enable_ext_polarity=true")
(set-option :config "theory.arr.enable_ext_arg=true")
(set-option :config "theory.arr.enable_witness=true")
(set-option :config "theory.fp.enabled=true")
(set-option :config "theory.fp.mode=1")
(set-option :config "theory.fp.bv_combination_enabled=true")
(set-option :config "theory.fp.bit_blast_mode=2")
(set-option :config "theory.fp.dpll.restart_strategy=3")
(set-option :config "theory.fp.dpll.restart_initial=200")
(set-option :config "theory.fp.dpll.restart_geometric_factor=1.5")
(set-option :config "theory.fp.dpll.branching_random_frequency=0.01")
(set-option :config "theory.fp.dpll.branching_initial_phase=0")
(set-option :config "theory.fp.dpll.branching_cache_phase=1")
(set-option :config "theory.fp.dpll.branching_random_invalidate_phase_cache=false")
(set-option :config "theory.fp.dpll.branching_random_ignore_polarity=true")
(set-option :config "theory.fp.dpll.ghost_filtering=false")
(set-option :config "theory.fp.dpll.glucose_var_activity=true")
(set-option :config "theory.fp.dpll.glucose_learnt_minimization=true")
(set-option :config "theory.fp.acdcl_conflict_generalization=2")
(set-option :config "theory.fp.interpolation_mode=0")
(set-option :config "theory.fp.acdcl_single_propagation_limit=0")
(set-option :config "theory.fp.acdcl_single_generalization_limit=0")
(set-option :config "theory.fp.acdcl_generalization_fair=true")
(set-option :config "theory.fp.minmax_zero_mode=1")
(set-option :config "theory.fp.to_bv_overflow_mode=0")
(set-option :config "theory.na.enabled=true")
(set-option :config "theory.na.permanent_lemmas=true")
(set-option :config "theory.na.eager_lemmas=false")
(set-option :config "theory.na.enable_tangent_lemmas_frontier=true")
(set-option :config "theory.na.tangent_lemmas_rat_approx=0")
(set-option :config "theory.na.tangent_lemmas_limit=0")
(set-option :config "theory.na.tangent_lemmas_enabled=true")
(set-option :config "theory.na.sat_check_enabled=true")
(set-option :config "theory.na.bound_lemmas_enabled=true")
(set-option :config "theory.na.nta_enabled=true")
(set-option :config "theory.na.nta_rat_approx=3")
(set-option :config "theory.na.nta_rat_approx_limit=10")
(set-option :config "theory.na.nta_sat_mode=1")
(set-option :config "theory.na.nta_eager=true")

(push 1)
(declare-fun __return_104@2 () (_ FloatingPoint 11 53))
(declare-fun __VERIFIER_nondet_double!2@ () (_ FloatingPoint 11 53))
(declare-fun |main::main__a@3| () (_ FloatingPoint 11 53))
(declare-fun |main::main____CPAchecker_TMP_0@3| () (_ BitVec 32))
(declare-fun |main::__tmp_1@3| () (_ FloatingPoint 11 53))
(declare-fun |main::inv__A@3| () (_ FloatingPoint 11 53))
(declare-fun |__ADDRESS_OF_main::inv__A_u@| () (_ BitVec 32))
(declare-fun |__ADDRESS_OF_main::inv__xi_u@| () (_ BitVec 32))
(declare-fun |main::inv__A_u$d@3| () (_ FloatingPoint 11 53))
(declare-fun |main::inv__A_u$i@3| () (_ BitVec 32))
(declare-fun |main::inv__exp@3| () (_ BitVec 32))
(declare-fun |main::inv__xi_u$d@3| () (_ FloatingPoint 11 53))
(declare-fun |main::inv__xi_u$i@3| () (_ BitVec 32))
(declare-fun |main::inv__xi_u$d@4| () (_ FloatingPoint 11 53))
(declare-fun |main::inv__xi_u$i@4| () (_ BitVec 32))
(declare-fun |main::inv__xi@3| () (_ FloatingPoint 11 53))
(declare-fun |main::inv__cond@3| () (_ BitVec 32))
(declare-fun |main::inv__xsi@3| () (_ FloatingPoint 11 53))
(declare-fun |main::inv__temp@3| () (_ FloatingPoint 11 53))
(declare-fun |main::inv____CPAchecker_TMP_0@3| () (_ BitVec 32))
(declare-fun |main::inv__cond@4| () (_ BitVec 32))
(declare-fun |main::inv__xi@4| () (_ FloatingPoint 11 53))
(declare-fun |main::inv__xsi@4| () (_ FloatingPoint 11 53))
(declare-fun |main::inv__temp@4| () (_ FloatingPoint 11 53))
(declare-fun |main::inv____CPAchecker_TMP_0@5| () (_ BitVec 32))
(declare-fun |main::inv__cond@5| () (_ BitVec 32))
(declare-fun |main::inv__xi@5| () (_ FloatingPoint 11 53))
(define-fun .3 () RoundingMode RNE)
(define-fun .8 () (_ BitVec 32) (_ bv0 32))
(define-fun .9 () (_ BitVec 32) (_ bv8 32))
(define-fun .10 () (_ FloatingPoint 11 53) (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000))
(define-fun .11 () (_ FloatingPoint 11 53) __return_104@2)
(define-fun .12 () Bool (= .11 .10))
(define-fun .13 () (_ FloatingPoint 11 53) __VERIFIER_nondet_double!2@)
(define-fun .14 () (_ FloatingPoint 11 53) |main::main__a@3|)
(define-fun .15 () Bool (= .13 .14))
(define-fun .16 () Bool (and .12 .15))
(define-fun .17 () (_ BitVec 32) (_ bv4 32))
(define-fun .18 () (_ FloatingPoint 11 53) (fp #b0 #b10000000011 #b0100000000000000000000000000000000000000000000000000))
(define-fun .19 () Bool (fp.leq .18 .14))
(define-fun .20 () (_ BitVec 32) (_ bv1 32))
(define-fun .22 () Bool (and .16 .19))
(define-fun .23 () Bool (not .19))
(define-fun .24 () Bool (and .16 .23))
(define-fun .25 () (_ FloatingPoint 11 53) (fp #b0 #b10000000011 #b1110000000000000000000000000000000000000000000000000))
(define-fun .26 () Bool (fp.leq .14 .25))
(define-fun .28 () Bool (and .22 .26))
(define-fun .29 () Bool (not .26))
(define-fun .30 () Bool (and .22 .29))
(define-fun .31 () Bool (or .24 .30))
(define-fun .32 () (_ BitVec 32) |main::main____CPAchecker_TMP_0@3|)
(define-fun .33 () Bool (= .32 .8))
(define-fun .34 () Bool (and .31 .33))
(define-fun .35 () Bool (= .32 .20))
(define-fun .36 () Bool (and .28 .35))
(define-fun .37 () Bool (or .34 .36))
(define-fun .38 () Bool (not .33))
(define-fun .40 () Bool (and .37 .38))
(define-fun .46 () (_ FloatingPoint 11 53) |main::__tmp_1@3|)
(define-fun .47 () Bool (= .14 .46))
(define-fun .48 () Bool (and .40 .47))
(define-fun .49 () (_ FloatingPoint 11 53) |main::inv__A@3|)
(define-fun .50 () Bool (= .46 .49))
(define-fun .51 () Bool (and .48 .50))
(define-fun .52 () (_ BitVec 32) |__ADDRESS_OF_main::inv__A_u@|)
(define-fun .53 () Bool (bvslt .8 .52))
(define-fun .54 () (_ BitVec 32) (bvurem .52 .17))
(define-fun .55 () Bool (= .54 .8))
(define-fun .57 () (_ BitVec 32) (bvadd .9 .52))
(define-fun .58 () Bool (bvslt .8 .57))
(define-fun .59 () Bool (and .53 .55))
(define-fun .60 () Bool (and .58 .59))
(define-fun .61 () Bool (and .51 .60))
(define-fun .62 () (_ BitVec 32) |__ADDRESS_OF_main::inv__xi_u@|)
(define-fun .63 () Bool (bvslt .57 .62))
(define-fun .64 () (_ BitVec 32) (bvurem .62 .17))
(define-fun .65 () Bool (= .64 .8))
(define-fun .67 () (_ BitVec 32) (bvadd .9 .62))
(define-fun .68 () Bool (bvslt .8 .67))
(define-fun .69 () Bool (and .63 .65))
(define-fun .70 () Bool (and .68 .69))
(define-fun .71 () Bool (and .61 .70))
(define-fun .72 () (_ FloatingPoint 11 53) |main::inv__A_u$d@3|)
(define-fun .73 () Bool (= .49 .72))
(define-fun .74 () (_ BitVec 64) (fp.as_ieee_bv .49))
(define-fun .75 () (_ BitVec 32) ((_ extract 31 0) .74))
(define-fun .76 () (_ BitVec 32) |main::inv__A_u$i@3|)
(define-fun .77 () Bool (= .75 .76))
(define-fun .78 () Bool (and .73 .77))
(define-fun .79 () Bool (and .71 .78))
(define-fun .80 () (_ BitVec 32) (_ bv2146435072 32))
(define-fun .82 () (_ BitVec 32) (bvand .80 .76))
(define-fun .83 () (_ BitVec 32) (_ bv20 32))
(define-fun .84 () (_ BitVec 32) (bvashr .82 .83))
(define-fun .85 () (_ BitVec 32) (_ bv1023 32))
(define-fun .87 () (_ BitVec 32) (_ bv4294966273 32))
(define-fun .89 () (_ BitVec 32) (bvadd .87 .84))
(define-fun .90 () (_ BitVec 32) |main::inv__exp@3|)
(define-fun .91 () Bool (= .89 .90))
(define-fun .92 () Bool (and .79 .91))
(define-fun .93 () (_ FloatingPoint 11 53) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000))
(define-fun .94 () (_ FloatingPoint 11 53) |main::inv__xi_u$d@3|)
(define-fun .95 () Bool (= .94 .93))
(define-fun .97 () (_ BitVec 32) |main::inv__xi_u$i@3|)
(define-fun .98 () Bool (= .97 .8))
(define-fun .99 () Bool (and .95 .98))
(define-fun .100 () Bool (and .92 .99))
(define-fun .102 () (_ BitVec 32) (bvneg .90))
(define-fun .103 () (_ BitVec 32) (bvadd .85 .102))
(define-fun .104 () (_ BitVec 32) (bvshl .103 .83))
(define-fun .106 () (_ BitVec 64) (fp.as_ieee_bv .94))
(define-fun .107 () (_ BitVec 32) ((_ extract 63 32) .106))
(define-fun .108 () (_ BitVec 64) (concat .107 .104))
(define-fun .109 () (_ FloatingPoint 11 53) ((_ to_fp 11 53) .108))
(define-fun .110 () (_ FloatingPoint 11 53) |main::inv__xi_u$d@4|)
(define-fun .111 () Bool (= .109 .110))
(define-fun .112 () (_ BitVec 32) |main::inv__xi_u$i@4|)
(define-fun .113 () Bool (= .104 .112))
(define-fun .114 () Bool (and .111 .113))
(define-fun .115 () Bool (and .100 .114))
(define-fun .116 () (_ FloatingPoint 11 53) |main::inv__xi@3|)
(define-fun .117 () Bool (= .110 .116))
(define-fun .118 () Bool (and .115 .117))
(define-fun .119 () (_ BitVec 32) |main::inv__cond@3|)
(define-fun .120 () Bool (= .119 .20))
(define-fun .121 () Bool (and .118 .120))
(define-fun .122 () Bool (= .119 .8))
(define-fun .124 () Bool (not .122))
(define-fun .125 () (_ FloatingPoint 11 53) (fp #b0 #b10000000000 #b0000000000000000000000000000000000000000000000000000))
(define-fun .126 () (_ FloatingPoint 11 53) (fp.mul .3 .116 .125))
(define-fun .127 () (_ FloatingPoint 11 53) (fp.mul .3 .49 .116))
(define-fun .128 () (_ FloatingPoint 11 53) (fp.mul .3 .116 .127))
(define-fun .129 () (_ FloatingPoint 11 53) (fp.sub .3 .126 .128))
(define-fun .130 () (_ FloatingPoint 11 53) |main::inv__xsi@3|)
(define-fun .131 () Bool (= .129 .130))
(define-fun .132 () Bool (and .124 .131))
(define-fun .133 () (_ FloatingPoint 11 53) (fp.sub .3 .130 .116))
(define-fun .134 () (_ FloatingPoint 11 53) |main::inv__temp@3|)
(define-fun .135 () Bool (= .133 .134))
(define-fun .136 () Bool (and .132 .135))
(define-fun .137 () (_ FloatingPoint 11 53) (fp #b0 #b01111011101 #b1011011111001101111111011001110101111011110110111011))
(define-fun .138 () Bool (fp.lt .137 .134))
(define-fun .140 () Bool (and .136 .138))
(define-fun .141 () Bool (not .138))
(define-fun .142 () Bool (and .136 .141))
(define-fun .143 () (_ FloatingPoint 11 53) (fp #b1 #b01111011101 #b1011011111001101111111011001110101111011110110111011))
(define-fun .144 () Bool (fp.lt .134 .143))
(define-fun .146 () Bool (and .142 .144))
(define-fun .147 () Bool (not .144))
(define-fun .148 () Bool (and .142 .147))
(define-fun .149 () (_ BitVec 32) |main::inv____CPAchecker_TMP_0@3|)
(define-fun .150 () Bool (= .149 .8))
(define-fun .151 () Bool (and .148 .150))
(define-fun .152 () Bool (or .140 .146))
(define-fun .153 () Bool (= .149 .20))
(define-fun .154 () Bool (and .152 .153))
(define-fun .155 () Bool (or .151 .154))
(define-fun .156 () (_ BitVec 32) |main::inv__cond@4|)
(define-fun .157 () Bool (= .149 .156))
(define-fun .158 () Bool (and .155 .157))
(define-fun .159 () (_ FloatingPoint 11 53) |main::inv__xi@4|)
(define-fun .160 () Bool (= .130 .159))
(define-fun .161 () Bool (and .158 .160))
(define-fun .198 () Bool (= .156 .8))
(define-fun .200 () Bool (not .198))
(define-fun .232 () Bool (and .121 .161))
(define-fun .267 () (_ FloatingPoint 11 53) (fp.mul .3 .125 .159))
(define-fun .268 () (_ FloatingPoint 11 53) (fp.mul .3 .49 .159))
(define-fun .269 () (_ FloatingPoint 11 53) (fp.mul .3 .159 .268))
(define-fun .270 () (_ FloatingPoint 11 53) (fp.sub .3 .267 .269))
(define-fun .271 () (_ FloatingPoint 11 53) |main::inv__xsi@4|)
(define-fun .272 () Bool (= .270 .271))
(define-fun .273 () Bool (and .200 .272))
(define-fun .274 () (_ FloatingPoint 11 53) (fp.sub .3 .271 .159))
(define-fun .275 () (_ FloatingPoint 11 53) |main::inv__temp@4|)
(define-fun .276 () Bool (= .274 .275))
(define-fun .277 () Bool (and .273 .276))
(define-fun .278 () Bool (fp.lt .137 .275))
(define-fun .280 () Bool (and .277 .278))
(define-fun .281 () Bool (not .278))
(define-fun .282 () Bool (and .277 .281))
(define-fun .283 () Bool (fp.lt .275 .143))
(define-fun .285 () Bool (and .282 .283))
(define-fun .286 () Bool (not .283))
(define-fun .287 () Bool (and .282 .286))
(define-fun .288 () (_ BitVec 32) |main::inv____CPAchecker_TMP_0@5|)
(define-fun .289 () Bool (= .288 .8))
(define-fun .290 () Bool (and .287 .289))
(define-fun .291 () Bool (or .280 .285))
(define-fun .292 () Bool (= .288 .20))
(define-fun .293 () Bool (and .291 .292))
(define-fun .294 () Bool (or .290 .293))
(define-fun .295 () (_ BitVec 32) |main::inv__cond@5|)
(define-fun .296 () Bool (= .288 .295))
(define-fun .297 () Bool (and .294 .296))
(define-fun .298 () (_ FloatingPoint 11 53) |main::inv__xi@5|)
(define-fun .299 () Bool (= .271 .298))
(define-fun .300 () Bool (and .297 .299))
(define-fun .323 () Bool (and .232 .300))
(assert .323)
(check-sat)