search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
186 stars 46 forks source link

Interpolation SigSev using Mathsat5 #210

Open baierd opened 4 years ago

baierd commented 4 years ago

There are currently 2 SigSevs in the buildbot table resulting from the use of interpolation with Mathsat5. I checked the queries with Mathsat directly and those result only in an error: (error "can't build ie-local interpolant") and not a SigSev. The error message is present in our ALLOWED_FAILURE_MESSAGES so this must have been encountered in the past. Is this a possible bug in our wrapper as it should not SigSev? (Also, what is an "ie-local" interpolant? :D @kfriedberger )

kfriedberger commented 4 years ago

Thanks for checking the Buildbot tables. This should really be done from time to time. :-) I don't think that this is a bug in the wrapper, but more a bug in MathSAT5. This is again a case where we would need a (small) C program to verify it directly via the native API.

I do not know the exact reason why MathSAT5 fails, but in some cases interpolation queries get hard when using UF, Array and BV theory, and then MathSAT5 gives up.

MartinSpiessl commented 4 years ago

To answer the question about ie-local, one could read http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_089.pdf:

Cimatti et al. [6] present a method to compute interpolants for linear rational arithmetic and difference logic. The method presented in this paper builds upon their interpolation technique for linear rational arithmetic. For theories combined via delayed theory combination, they show how to compute interpolants by transforming a proof into a so-called ie-local proof. In these proofs, mixed equalities are close to the leaves of the proof tree and splitting them is cheap since the proof trees that have to be duplicated are small. A variant of this restricted search strategy is used by MathSAT [14] and CSIsat [1]

further information can be found in [6]: https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_30.pdf

First, we control the branching and learning heuristics of the SMT solver to ensure that the generated resolution proof of unsatisfiability P has a property that we call locality wrt. interface equalities. We say that P is local wrt. interface equalities (ie -local) if the interface equalities occur only in subproofs P_{ie}^i of P

So ie probably stands for "interface equalities"

baierd commented 4 years ago

Thank you for the information. Unfortunately this does not seem useful for us.

baierd commented 4 years ago

So it seems that the problem is the try to get the interpolants back.

If you try the following SMTLIB2 example taken from the CPAchecker-Mathsat-Query and parse it in the current mathsat version via ./mathsat-5.6.4-reentrant -input=smt2 <FILENAME.smt2 you get the mentioned error. Removing (get-interpolant ...) in the last line removes the error. Changing the wanted interpolant does not change anything.

SMTLIB2 example:

;; MathSAT API call trace
;; generated on Fri 16 Oct 2020 05:24:52 PM CEST
(set-option :global-declarations true)
(set-option :config "verbosity=0")
(set-option :config "proof_generation=true")
(set-option :config "interpolation=true")
(set-option :config "model_generation=true")
(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=false")
(set-option :config "preprocessor.toplevel_propagation_limit=0")
(set-option :config "preprocessor.simplification=23")
(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=false")
(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.minmax_zero_mode=1")
(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.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 |main::nodecount@2| () (_ BitVec 32))
(declare-fun |__ADDRESS_OF_main::distance@| () (_ BitVec 32))
(declare-fun |__VERIFIER_assert::cond@2| () (_ BitVec 32))
(declare-fun |main::i@21| () (_ BitVec 32))
(declare-fun *int@9 () (Array (_ BitVec 32) (_ BitVec 32)))
(define-fun .8 () (_ BitVec 32) (_ bv0 32))
(define-fun .14 () (_ BitVec 32) |main::nodecount@2|)
(define-fun .37 () (_ BitVec 32) (_ bv1 32))
(define-fun .43 () (_ BitVec 32) (_ bv2 32))
(define-fun .387 () (_ BitVec 32) |__ADDRESS_OF_main::distance@|)
(define-fun .440 () (_ BitVec 1) (_ bv1 1))
(define-fun .445 () (_ BitVec 32) |__VERIFIER_assert::cond@2|)
(define-fun .448 () Bool (= .445 .8))
(define-fun .9743 () (_ BitVec 32) |main::i@21|)
(define-fun .9748 () (_ BitVec 32) (bvshl .9743 .43))
(define-fun .9749 () (_ BitVec 32) (bvadd .387 .9748))
(define-fun .12644 () Bool (bvslt .9743 .14))
(define-fun .24842 () (Array (_ BitVec 32) (_ BitVec 32)) *int@9)
(define-fun .29124 () (_ BitVec 32) (select .24842 .9749))
(define-fun .29125 () (_ BitVec 1) ((_ extract 31 31) .29124))
(define-fun .29126 () Bool (= .29125 .440))
(define-fun .29212 () Bool (not .29126))
(define-fun .29213 () (_ BitVec 32) (ite .29212 .37 .8))
(define-fun .29214 () Bool (= .445 .29213))
(define-fun .29215 () Bool (and .12644 .29214))
(define-fun .29216 () Bool (and .448 .29215))
(assert (! .29216 :interpolation-group .g0))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g0))
(declare-fun INFINITY@2 () (_ BitVec 32))
(declare-fun |main::edgecount@2| () (_ BitVec 32))
(declare-fun |main::source@2| () (_ BitVec 32))
(declare-fun |__ADDRESS_OF_main::Source@| () (_ BitVec 32))
(declare-fun *int@1 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun |__ADDRESS_OF_main::Dest@| () (_ BitVec 32))
(declare-fun |__ADDRESS_OF_main::Weight@| () (_ BitVec 32))
(declare-fun |main::i@3| () (_ BitVec 32))
(define-fun .9 () (_ BitVec 32) (_ bv4 32))
(define-fun .10 () (_ BitVec 32) (_ bv899 32))
(define-fun .11 () (_ BitVec 32) INFINITY@2)
(define-fun .12 () Bool (= .11 .10))
(define-fun .13 () (_ BitVec 32) (_ bv5 32))
(define-fun .15 () Bool (= .14 .13))
(define-fun .16 () Bool (and .12 .15))
(define-fun .17 () (_ BitVec 32) (_ bv20 32))
(define-fun .18 () (_ BitVec 32) |main::edgecount@2|)
(define-fun .19 () Bool (= .18 .17))
(define-fun .20 () Bool (and .16 .19))
(define-fun .21 () (_ BitVec 32) |main::source@2|)
(define-fun .22 () Bool (= .21 .8))
(define-fun .23 () Bool (and .20 .22))
(define-fun .24 () (_ BitVec 32) (_ bv80 32))
(define-fun .25 () (_ BitVec 32) |__ADDRESS_OF_main::Source@|)
(define-fun .26 () Bool (bvslt .8 .25))
(define-fun .27 () (_ BitVec 32) (bvurem .25 .9))
(define-fun .28 () Bool (= .27 .8))
(define-fun .30 () (_ BitVec 32) (bvadd .24 .25))
(define-fun .31 () Bool (bvslt .8 .30))
(define-fun .34 () (Array (_ BitVec 32) (_ BitVec 32)) *int@1)
(define-fun .35 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .25 .8))
(define-fun .36 () Bool (= .34 .35))
(define-fun .39 () (_ BitVec 32) (bvadd .9 .25))
(define-fun .40 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .39 .9))
(define-fun .41 () Bool (= .34 .40))
(define-fun .42 () Bool (and .36 .41))
(define-fun .44 () (_ BitVec 32) (_ bv8 32))
(define-fun .46 () (_ BitVec 32) (bvadd .44 .25))
(define-fun .47 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .46 .37))
(define-fun .48 () Bool (= .34 .47))
(define-fun .49 () Bool (and .42 .48))
(define-fun .50 () (_ BitVec 32) (_ bv3 32))
(define-fun .51 () (_ BitVec 32) (_ bv12 32))
(define-fun .53 () (_ BitVec 32) (bvadd .51 .25))
(define-fun .54 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .53 .37))
(define-fun .55 () Bool (= .34 .54))
(define-fun .56 () Bool (and .49 .55))
(define-fun .57 () (_ BitVec 32) (_ bv16 32))
(define-fun .59 () (_ BitVec 32) (bvadd .57 .25))
(define-fun .60 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .59 .8))
(define-fun .61 () Bool (= .34 .60))
(define-fun .62 () Bool (and .56 .61))
(define-fun .64 () (_ BitVec 32) (bvadd .17 .25))
(define-fun .65 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .64 .8))
(define-fun .66 () Bool (= .34 .65))
(define-fun .67 () Bool (and .62 .66))
(define-fun .68 () (_ BitVec 32) (_ bv6 32))
(define-fun .69 () (_ BitVec 32) (_ bv24 32))
(define-fun .71 () (_ BitVec 32) (bvadd .69 .25))
(define-fun .72 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .71 .37))
(define-fun .73 () Bool (= .34 .72))
(define-fun .74 () Bool (and .67 .73))
(define-fun .75 () (_ BitVec 32) (_ bv7 32))
(define-fun .76 () (_ BitVec 32) (_ bv28 32))
(define-fun .78 () (_ BitVec 32) (bvadd .76 .25))
(define-fun .79 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .78 .50))
(define-fun .80 () Bool (= .34 .79))
(define-fun .81 () Bool (and .74 .80))
(define-fun .82 () (_ BitVec 32) (_ bv32 32))
(define-fun .84 () (_ BitVec 32) (bvadd .82 .25))
(define-fun .85 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .84 .9))
(define-fun .86 () Bool (= .34 .85))
(define-fun .87 () Bool (and .81 .86))
(define-fun .88 () (_ BitVec 32) (_ bv9 32))
(define-fun .89 () (_ BitVec 32) (_ bv36 32))
(define-fun .91 () (_ BitVec 32) (bvadd .89 .25))
(define-fun .92 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .91 .9))
(define-fun .93 () Bool (= .34 .92))
(define-fun .94 () Bool (and .87 .93))
(define-fun .95 () (_ BitVec 32) (_ bv10 32))
(define-fun .96 () (_ BitVec 32) (_ bv40 32))
(define-fun .98 () (_ BitVec 32) (bvadd .96 .25))
(define-fun .99 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .98 .43))
(define-fun .100 () Bool (= .34 .99))
(define-fun .101 () Bool (and .94 .100))
(define-fun .102 () (_ BitVec 32) (_ bv11 32))
(define-fun .103 () (_ BitVec 32) (_ bv44 32))
(define-fun .105 () (_ BitVec 32) (bvadd .103 .25))
(define-fun .106 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .105 .43))
(define-fun .107 () Bool (= .34 .106))
(define-fun .108 () Bool (and .101 .107))
(define-fun .109 () (_ BitVec 32) (_ bv48 32))
(define-fun .111 () (_ BitVec 32) (bvadd .109 .25))
(define-fun .112 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .111 .50))
(define-fun .113 () Bool (= .34 .112))
(define-fun .114 () Bool (and .108 .113))
(define-fun .115 () (_ BitVec 32) (_ bv13 32))
(define-fun .116 () (_ BitVec 32) (_ bv52 32))
(define-fun .118 () (_ BitVec 32) (bvadd .116 .25))
(define-fun .119 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .118 .8))
(define-fun .120 () Bool (= .34 .119))
(define-fun .121 () Bool (and .114 .120))
(define-fun .122 () (_ BitVec 32) (_ bv14 32))
(define-fun .123 () (_ BitVec 32) (_ bv56 32))
(define-fun .125 () (_ BitVec 32) (bvadd .123 .25))
(define-fun .126 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .125 .8))
(define-fun .127 () Bool (= .34 .126))
(define-fun .128 () Bool (and .121 .127))
(define-fun .129 () (_ BitVec 32) (_ bv15 32))
(define-fun .130 () (_ BitVec 32) (_ bv60 32))
(define-fun .132 () (_ BitVec 32) (bvadd .130 .25))
(define-fun .133 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .132 .50))
(define-fun .134 () Bool (= .34 .133))
(define-fun .135 () Bool (and .128 .134))
(define-fun .136 () (_ BitVec 32) (_ bv64 32))
(define-fun .138 () (_ BitVec 32) (bvadd .136 .25))
(define-fun .139 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .138 .37))
(define-fun .140 () Bool (= .34 .139))
(define-fun .141 () Bool (and .135 .140))
(define-fun .142 () (_ BitVec 32) (_ bv17 32))
(define-fun .143 () (_ BitVec 32) (_ bv68 32))
(define-fun .145 () (_ BitVec 32) (bvadd .143 .25))
(define-fun .146 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .145 .43))
(define-fun .147 () Bool (= .34 .146))
(define-fun .148 () Bool (and .141 .147))
(define-fun .149 () (_ BitVec 32) (_ bv18 32))
(define-fun .150 () (_ BitVec 32) (_ bv72 32))
(define-fun .152 () (_ BitVec 32) (bvadd .150 .25))
(define-fun .153 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .152 .43))
(define-fun .154 () Bool (= .34 .153))
(define-fun .155 () Bool (and .148 .154))
(define-fun .156 () (_ BitVec 32) (_ bv19 32))
(define-fun .157 () (_ BitVec 32) (_ bv76 32))
(define-fun .159 () (_ BitVec 32) (bvadd .157 .25))
(define-fun .160 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .159 .50))
(define-fun .161 () Bool (= .34 .160))
(define-fun .162 () Bool (and .155 .161))
(define-fun .163 () Bool (and .26 .28))
(define-fun .164 () Bool (and .31 .163))
(define-fun .165 () Bool (and .162 .164))
(define-fun .166 () Bool (and .23 .165))
(define-fun .167 () (_ BitVec 32) |__ADDRESS_OF_main::Dest@|)
(define-fun .168 () Bool (bvslt .30 .167))
(define-fun .169 () (_ BitVec 32) (bvurem .167 .9))
(define-fun .170 () Bool (= .169 .8))
(define-fun .172 () (_ BitVec 32) (bvadd .24 .167))
(define-fun .173 () Bool (bvslt .8 .172))
(define-fun .176 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .167 .37))
(define-fun .177 () Bool (= .34 .176))
(define-fun .179 () (_ BitVec 32) (bvadd .9 .167))
(define-fun .180 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .179 .50))
(define-fun .181 () Bool (= .34 .180))
(define-fun .182 () Bool (and .177 .181))
(define-fun .184 () (_ BitVec 32) (bvadd .44 .167))
(define-fun .185 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .184 .9))
(define-fun .186 () Bool (= .34 .185))
(define-fun .187 () Bool (and .182 .186))
(define-fun .189 () (_ BitVec 32) (bvadd .51 .167))
(define-fun .190 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .189 .37))
(define-fun .191 () Bool (= .34 .190))
(define-fun .192 () Bool (and .187 .191))
(define-fun .194 () (_ BitVec 32) (bvadd .57 .167))
(define-fun .195 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .194 .37))
(define-fun .196 () Bool (= .34 .195))
(define-fun .197 () Bool (and .192 .196))
(define-fun .199 () (_ BitVec 32) (bvadd .17 .167))
(define-fun .200 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .199 .9))
(define-fun .201 () Bool (= .34 .200))
(define-fun .202 () Bool (and .197 .201))
(define-fun .204 () (_ BitVec 32) (bvadd .69 .167))
(define-fun .205 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .204 .50))
(define-fun .206 () Bool (= .34 .205))
(define-fun .207 () Bool (and .202 .206))
(define-fun .209 () (_ BitVec 32) (bvadd .76 .167))
(define-fun .210 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .209 .9))
(define-fun .211 () Bool (= .34 .210))
(define-fun .212 () Bool (and .207 .211))
(define-fun .214 () (_ BitVec 32) (bvadd .82 .167))
(define-fun .215 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .214 .50))
(define-fun .216 () Bool (= .34 .215))
(define-fun .217 () Bool (and .212 .216))
(define-fun .219 () (_ BitVec 32) (bvadd .89 .167))
(define-fun .220 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .219 .8))
(define-fun .221 () Bool (= .34 .220))
(define-fun .222 () Bool (and .217 .221))
(define-fun .224 () (_ BitVec 32) (bvadd .96 .167))
(define-fun .225 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .224 .8))
(define-fun .226 () Bool (= .34 .225))
(define-fun .227 () Bool (and .222 .226))
(define-fun .229 () (_ BitVec 32) (bvadd .103 .167))
(define-fun .230 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .229 .8))
(define-fun .231 () Bool (= .34 .230))
(define-fun .232 () Bool (and .227 .231))
(define-fun .234 () (_ BitVec 32) (bvadd .109 .167))
(define-fun .235 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .234 .8))
(define-fun .236 () Bool (= .34 .235))
(define-fun .237 () Bool (and .232 .236))
(define-fun .239 () (_ BitVec 32) (bvadd .116 .167))
(define-fun .240 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .239 .43))
(define-fun .241 () Bool (= .34 .240))
(define-fun .242 () Bool (and .237 .241))
(define-fun .244 () (_ BitVec 32) (bvadd .123 .167))
(define-fun .245 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .244 .50))
(define-fun .246 () Bool (= .34 .245))
(define-fun .247 () Bool (and .242 .246))
(define-fun .249 () (_ BitVec 32) (bvadd .130 .167))
(define-fun .250 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .249 .8))
(define-fun .251 () Bool (= .34 .250))
(define-fun .252 () Bool (and .247 .251))
(define-fun .254 () (_ BitVec 32) (bvadd .136 .167))
(define-fun .255 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .254 .43))
(define-fun .256 () Bool (= .34 .255))
(define-fun .257 () Bool (and .252 .256))
(define-fun .259 () (_ BitVec 32) (bvadd .143 .167))
(define-fun .260 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .259 .37))
(define-fun .261 () Bool (= .34 .260))
(define-fun .262 () Bool (and .257 .261))
(define-fun .264 () (_ BitVec 32) (bvadd .150 .167))
(define-fun .265 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .264 .8))
(define-fun .266 () Bool (= .34 .265))
(define-fun .267 () Bool (and .262 .266))
(define-fun .269 () (_ BitVec 32) (bvadd .157 .167))
(define-fun .270 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .269 .9))
(define-fun .271 () Bool (= .34 .270))
(define-fun .272 () Bool (and .267 .271))
(define-fun .273 () Bool (and .168 .170))
(define-fun .274 () Bool (and .173 .273))
(define-fun .275 () Bool (and .272 .274))
(define-fun .276 () Bool (and .166 .275))
(define-fun .277 () (_ BitVec 32) |__ADDRESS_OF_main::Weight@|)
(define-fun .278 () Bool (bvslt .172 .277))
(define-fun .279 () (_ BitVec 32) (bvurem .277 .9))
(define-fun .280 () Bool (= .279 .8))
(define-fun .282 () (_ BitVec 32) (bvadd .24 .277))
(define-fun .283 () Bool (bvslt .8 .282))
(define-fun .286 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .277 .8))
(define-fun .287 () Bool (= .34 .286))
(define-fun .289 () (_ BitVec 32) (bvadd .9 .277))
(define-fun .290 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .289 .37))
(define-fun .291 () Bool (= .34 .290))
(define-fun .292 () Bool (and .287 .291))
(define-fun .294 () (_ BitVec 32) (bvadd .44 .277))
(define-fun .295 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .294 .43))
(define-fun .296 () Bool (= .34 .295))
(define-fun .297 () Bool (and .292 .296))
(define-fun .299 () (_ BitVec 32) (bvadd .51 .277))
(define-fun .300 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .299 .50))
(define-fun .301 () Bool (= .34 .300))
(define-fun .302 () Bool (and .297 .301))
(define-fun .304 () (_ BitVec 32) (bvadd .57 .277))
(define-fun .305 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .304 .9))
(define-fun .306 () Bool (= .34 .305))
(define-fun .307 () Bool (and .302 .306))
(define-fun .309 () (_ BitVec 32) (bvadd .17 .277))
(define-fun .310 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .309 .13))
(define-fun .311 () Bool (= .34 .310))
(define-fun .312 () Bool (and .307 .311))
(define-fun .314 () (_ BitVec 32) (bvadd .69 .277))
(define-fun .315 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .314 .68))
(define-fun .316 () Bool (= .34 .315))
(define-fun .317 () Bool (and .312 .316))
(define-fun .319 () (_ BitVec 32) (bvadd .76 .277))
(define-fun .320 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .319 .75))
(define-fun .321 () Bool (= .34 .320))
(define-fun .322 () Bool (and .317 .321))
(define-fun .324 () (_ BitVec 32) (bvadd .82 .277))
(define-fun .325 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .324 .44))
(define-fun .326 () Bool (= .34 .325))
(define-fun .327 () Bool (and .322 .326))
(define-fun .329 () (_ BitVec 32) (bvadd .89 .277))
(define-fun .330 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .329 .88))
(define-fun .331 () Bool (= .34 .330))
(define-fun .332 () Bool (and .327 .331))
(define-fun .334 () (_ BitVec 32) (bvadd .96 .277))
(define-fun .335 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .334 .95))
(define-fun .336 () Bool (= .34 .335))
(define-fun .337 () Bool (and .332 .336))
(define-fun .339 () (_ BitVec 32) (bvadd .103 .277))
(define-fun .340 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .339 .102))
(define-fun .341 () Bool (= .34 .340))
(define-fun .342 () Bool (and .337 .341))
(define-fun .344 () (_ BitVec 32) (bvadd .109 .277))
(define-fun .345 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .344 .51))
(define-fun .346 () Bool (= .34 .345))
(define-fun .347 () Bool (and .342 .346))
(define-fun .349 () (_ BitVec 32) (bvadd .116 .277))
(define-fun .350 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .349 .115))
(define-fun .351 () Bool (= .34 .350))
(define-fun .352 () Bool (and .347 .351))
(define-fun .354 () (_ BitVec 32) (bvadd .123 .277))
(define-fun .355 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .354 .122))
(define-fun .356 () Bool (= .34 .355))
(define-fun .357 () Bool (and .352 .356))
(define-fun .359 () (_ BitVec 32) (bvadd .130 .277))
(define-fun .360 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .359 .129))
(define-fun .361 () Bool (= .34 .360))
(define-fun .362 () Bool (and .357 .361))
(define-fun .364 () (_ BitVec 32) (bvadd .136 .277))
(define-fun .365 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .364 .57))
(define-fun .366 () Bool (= .34 .365))
(define-fun .367 () Bool (and .362 .366))
(define-fun .369 () (_ BitVec 32) (bvadd .143 .277))
(define-fun .370 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .369 .142))
(define-fun .371 () Bool (= .34 .370))
(define-fun .372 () Bool (and .367 .371))
(define-fun .374 () (_ BitVec 32) (bvadd .150 .277))
(define-fun .375 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .374 .149))
(define-fun .376 () Bool (= .34 .375))
(define-fun .377 () Bool (and .372 .376))
(define-fun .379 () (_ BitVec 32) (bvadd .157 .277))
(define-fun .380 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .379 .156))
(define-fun .381 () Bool (= .34 .380))
(define-fun .382 () Bool (and .377 .381))
(define-fun .383 () Bool (and .278 .280))
(define-fun .384 () Bool (and .283 .383))
(define-fun .385 () Bool (and .382 .384))
(define-fun .386 () Bool (and .276 .385))
(define-fun .388 () Bool (bvslt .282 .387))
(define-fun .389 () (_ BitVec 32) (bvurem .387 .9))
(define-fun .390 () Bool (= .389 .8))
(define-fun .392 () (_ BitVec 32) (bvadd .17 .387))
(define-fun .393 () Bool (bvslt .8 .392))
(define-fun .404 () Bool (and .388 .390))
(define-fun .405 () Bool (and .393 .404))
(define-fun .406 () Bool (and .386 .405))
(define-fun .407 () (_ BitVec 32) |main::i@3|)
(define-fun .408 () Bool (= .407 .8))
(define-fun .409 () Bool (and .406 .408))
(assert (! .409 :interpolation-group .g1))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g1))
(declare-fun |main::i@20| () (_ BitVec 32))
(define-fun .8683 () (_ BitVec 32) |main::i@20|)
(define-fun .9747 () Bool (= .9743 .8))
(define-fun .13142 () Bool (bvslt .8683 .18))
(define-fun .13144 () Bool (not .13142))
(define-fun .13145 () Bool (and .9747 .13144))
(assert (! .13145 :interpolation-group .g2))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g2))
(declare-fun |main::i@4| () (_ BitVec 32))
(declare-fun *int@2 () (Array (_ BitVec 32) (_ BitVec 32)))
(define-fun .410 () Bool (bvslt .407 .14))
(define-fun .413 () (_ BitVec 32) |main::i@4|)
(define-fun .665 () Bool (= .21 .407))
(define-fun .667 () Bool (and .410 .665))
(define-fun .668 () Bool (not .665))
(define-fun .669 () Bool (and .410 .668))
(define-fun .671 () (_ BitVec 32) (bvshl .407 .43))
(define-fun .672 () (_ BitVec 32) (bvadd .387 .671))
(define-fun .673 () (Array (_ BitVec 32) (_ BitVec 32)) *int@2)
(define-fun .674 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .672 .11))
(define-fun .675 () Bool (= .673 .674))
(define-fun .676 () Bool (and .669 .675))
(define-fun .677 () (Array (_ BitVec 32) (_ BitVec 32)) (store .34 .672 .8))
(define-fun .678 () Bool (= .673 .677))
(define-fun .679 () Bool (and .667 .678))
(define-fun .680 () Bool (or .676 .679))
(define-fun .682 () (_ BitVec 32) (bvadd .37 .407))
(define-fun .683 () Bool (= .413 .682))
(define-fun .684 () Bool (and .680 .683))
(assert (! .684 :interpolation-group .g3))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g3))
(declare-fun |main::i@19| () (_ BitVec 32))
(declare-fun |main::x@14| () (_ BitVec 32))
(declare-fun |main::y@14| () (_ BitVec 32))
(define-fun .7785 () (_ BitVec 32) |main::i@19|)
(define-fun .7790 () (_ BitVec 32) (bvshl .7785 .43))
(define-fun .7795 () (_ BitVec 32) (bvadd .37 .7785))
(define-fun .8684 () Bool (= .7795 .8683))
(define-fun .13000 () Bool (bvslt .7785 .18))
(define-fun .13025 () (_ BitVec 32) (bvadd .167 .7790))
(define-fun .13030 () (_ BitVec 32) (bvadd .25 .7790))
(define-fun .13043 () (_ BitVec 32) (bvadd .277 .7790))
(define-fun .14743 () (_ BitVec 32) |main::x@14|)
(define-fun .14748 () (_ BitVec 32) |main::y@14|)
(define-fun .14752 () (_ BitVec 32) (bvshl .14743 .43))
(define-fun .14753 () (_ BitVec 32) (bvadd .387 .14752))
(define-fun .14756 () (_ BitVec 32) (bvshl .14748 .43))
(define-fun .14757 () (_ BitVec 32) (bvadd .387 .14756))
(define-fun .29036 () (_ BitVec 32) (select .24842 .13025))
(define-fun .29037 () Bool (= .14743 .29036))
(define-fun .29038 () Bool (and .13000 .29037))
(define-fun .29039 () (_ BitVec 32) (select .24842 .13030))
(define-fun .29040 () Bool (= .14748 .29039))
(define-fun .29041 () Bool (and .29038 .29040))
(define-fun .29042 () (_ BitVec 32) (select .24842 .14753))
(define-fun .29043 () (_ BitVec 32) (select .24842 .14757))
(define-fun .29044 () (_ BitVec 32) (select .24842 .13043))
(define-fun .29045 () (_ BitVec 32) (bvadd .29043 .29044))
(define-fun .29046 () Bool (bvslt .29045 .29042))
(define-fun .29049 () Bool (not .29046))
(define-fun .29050 () Bool (and .29041 .29049))
(define-fun .29051 () Bool (and .8684 .29050))
(assert (! .29051 :interpolation-group .g4))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g4))
(declare-fun |main::i@5| () (_ BitVec 32))
(declare-fun *int@3 () (Array (_ BitVec 32) (_ BitVec 32)))
(define-fun .416 () Bool (bvslt .413 .14))
(define-fun .419 () (_ BitVec 32) |main::i@5|)
(define-fun .826 () Bool (= .21 .413))
(define-fun .839 () Bool (not .826))
(define-fun .975 () Bool (and .416 .826))
(define-fun .976 () Bool (and .416 .839))
(define-fun .978 () (_ BitVec 32) (bvshl .413 .43))
(define-fun .979 () (_ BitVec 32) (bvadd .387 .978))
(define-fun .980 () (Array (_ BitVec 32) (_ BitVec 32)) *int@3)
(define-fun .981 () (Array (_ BitVec 32) (_ BitVec 32)) (store .673 .979 .11))
(define-fun .982 () Bool (= .980 .981))
(define-fun .983 () Bool (and .976 .982))
(define-fun .984 () (Array (_ BitVec 32) (_ BitVec 32)) (store .673 .979 .8))
(define-fun .985 () Bool (= .980 .984))
(define-fun .986 () Bool (and .975 .985))
(define-fun .987 () Bool (or .983 .986))
(define-fun .989 () (_ BitVec 32) (bvadd .37 .413))
(define-fun .990 () Bool (= .419 .989))
(define-fun .991 () Bool (and .987 .990))
(assert (! .991 :interpolation-group .g5))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g5))
(declare-fun |main::i@18| () (_ BitVec 32))
(declare-fun |main::x@13| () (_ BitVec 32))
(declare-fun |main::y@13| () (_ BitVec 32))
(define-fun .7057 () (_ BitVec 32) |main::i@18|)
(define-fun .7062 () (_ BitVec 32) (bvshl .7057 .43))
(define-fun .7067 () (_ BitVec 32) (bvadd .37 .7057))
(define-fun .7786 () Bool (= .7067 .7785))
(define-fun .10165 () Bool (bvslt .7057 .18))
(define-fun .10190 () (_ BitVec 32) (bvadd .167 .7062))
(define-fun .10195 () (_ BitVec 32) (bvadd .25 .7062))
(define-fun .10208 () (_ BitVec 32) (bvadd .277 .7062))
(define-fun .13171 () (_ BitVec 32) |main::x@13|)
(define-fun .13176 () (_ BitVec 32) |main::y@13|)
(define-fun .13180 () (_ BitVec 32) (bvshl .13171 .43))
(define-fun .13181 () (_ BitVec 32) (bvadd .387 .13180))
(define-fun .13184 () (_ BitVec 32) (bvshl .13176 .43))
(define-fun .13185 () (_ BitVec 32) (bvadd .387 .13184))
(define-fun .26174 () (_ BitVec 32) (select .24842 .10190))
(define-fun .26175 () Bool (= .13171 .26174))
(define-fun .26176 () Bool (and .10165 .26175))
(define-fun .26177 () (_ BitVec 32) (select .24842 .10195))
(define-fun .26178 () Bool (= .13176 .26177))
(define-fun .26179 () Bool (and .26176 .26178))
(define-fun .26180 () (_ BitVec 32) (select .24842 .13181))
(define-fun .26181 () (_ BitVec 32) (select .24842 .13185))
(define-fun .26182 () (_ BitVec 32) (select .24842 .10208))
(define-fun .26183 () (_ BitVec 32) (bvadd .26181 .26182))
(define-fun .26184 () Bool (bvslt .26183 .26180))
(define-fun .26187 () Bool (not .26184))
(define-fun .26188 () Bool (and .26179 .26187))
(define-fun .26189 () Bool (and .7786 .26188))
(assert (! .26189 :interpolation-group .g6))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g6))
(declare-fun |main::i@6| () (_ BitVec 32))
(declare-fun *int@4 () (Array (_ BitVec 32) (_ BitVec 32)))
(define-fun .425 () (_ BitVec 32) |main::i@6|)
(define-fun .714 () Bool (bvslt .419 .14))
(define-fun .993 () Bool (= .21 .419))
(define-fun .1322 () Bool (not .993))
(define-fun .1637 () Bool (and .714 .993))
(define-fun .1638 () Bool (and .714 .1322))
(define-fun .1640 () (_ BitVec 32) (bvshl .419 .43))
(define-fun .1641 () (_ BitVec 32) (bvadd .387 .1640))
(define-fun .1642 () (Array (_ BitVec 32) (_ BitVec 32)) *int@4)
(define-fun .1643 () (Array (_ BitVec 32) (_ BitVec 32)) (store .980 .1641 .11))
(define-fun .1644 () Bool (= .1642 .1643))
(define-fun .1645 () Bool (and .1638 .1644))
(define-fun .1646 () (Array (_ BitVec 32) (_ BitVec 32)) (store .980 .1641 .8))
(define-fun .1647 () Bool (= .1642 .1646))
(define-fun .1648 () Bool (and .1637 .1647))
(define-fun .1649 () Bool (or .1645 .1648))
(define-fun .1651 () (_ BitVec 32) (bvadd .37 .419))
(define-fun .1652 () Bool (= .425 .1651))
(define-fun .1653 () Bool (and .1649 .1652))
(assert (! .1653 :interpolation-group .g7))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g7))
(declare-fun |main::i@17| () (_ BitVec 32))
(declare-fun |main::x@12| () (_ BitVec 32))
(declare-fun |main::y@12| () (_ BitVec 32))
(define-fun .6204 () (_ BitVec 32) |main::i@17|)
(define-fun .6209 () (_ BitVec 32) (bvshl .6204 .43))
(define-fun .6214 () (_ BitVec 32) (bvadd .37 .6204))
(define-fun .7058 () Bool (= .6214 .7057))
(define-fun .10036 () Bool (bvslt .6204 .18))
(define-fun .10061 () (_ BitVec 32) (bvadd .167 .6209))
(define-fun .10066 () (_ BitVec 32) (bvadd .25 .6209))
(define-fun .10079 () (_ BitVec 32) (bvadd .277 .6209))
(define-fun .13027 () (_ BitVec 32) |main::x@12|)
(define-fun .13032 () (_ BitVec 32) |main::y@12|)
(define-fun .13036 () (_ BitVec 32) (bvshl .13027 .43))
(define-fun .13037 () (_ BitVec 32) (bvadd .387 .13036))
(define-fun .13040 () (_ BitVec 32) (bvshl .13032 .43))
(define-fun .13041 () (_ BitVec 32) (bvadd .387 .13040))
(define-fun .26026 () (_ BitVec 32) (select .24842 .10061))
(define-fun .26027 () Bool (= .13027 .26026))
(define-fun .26028 () Bool (and .10036 .26027))
(define-fun .26029 () (_ BitVec 32) (select .24842 .10066))
(define-fun .26030 () Bool (= .13032 .26029))
(define-fun .26031 () Bool (and .26028 .26030))
(define-fun .26032 () (_ BitVec 32) (select .24842 .13037))
(define-fun .26033 () (_ BitVec 32) (select .24842 .13041))
(define-fun .26034 () (_ BitVec 32) (select .24842 .10079))
(define-fun .26035 () (_ BitVec 32) (bvadd .26033 .26034))
(define-fun .26036 () Bool (bvslt .26035 .26032))
(define-fun .26039 () Bool (not .26036))
(define-fun .26040 () Bool (and .26031 .26039))
(define-fun .26041 () Bool (and .7058 .26040))
(assert (! .26041 :interpolation-group .g8))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g8))
(declare-fun |main::i@7| () (_ BitVec 32))
(declare-fun *int@5 () (Array (_ BitVec 32) (_ BitVec 32)))
(define-fun .428 () Bool (bvslt .425 .14))
(define-fun .435 () (_ BitVec 32) (bvshl .425 .43))
(define-fun .436 () (_ BitVec 32) (bvadd .387 .435))
(define-fun .724 () (_ BitVec 32) |main::i@7|)
(define-fun .1655 () Bool (= .21 .425))
(define-fun .1715 () Bool (not .1655))
(define-fun .2520 () Bool (and .428 .1655))
(define-fun .2521 () Bool (and .428 .1715))
(define-fun .2522 () (Array (_ BitVec 32) (_ BitVec 32)) *int@5)
(define-fun .2523 () (Array (_ BitVec 32) (_ BitVec 32)) (store .1642 .436 .11))
(define-fun .2524 () Bool (= .2522 .2523))
(define-fun .2525 () Bool (and .2521 .2524))
(define-fun .2526 () (Array (_ BitVec 32) (_ BitVec 32)) (store .1642 .436 .8))
(define-fun .2527 () Bool (= .2522 .2526))
(define-fun .2528 () Bool (and .2520 .2527))
(define-fun .2529 () Bool (or .2525 .2528))
(define-fun .2531 () (_ BitVec 32) (bvadd .37 .425))
(define-fun .2532 () Bool (= .724 .2531))
(define-fun .2533 () Bool (and .2529 .2532))
(assert (! .2533 :interpolation-group .g9))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g9))
(declare-fun |main::i@16| () (_ BitVec 32))
(declare-fun |main::x@11| () (_ BitVec 32))
(declare-fun |main::y@11| () (_ BitVec 32))
(define-fun .5294 () (_ BitVec 32) |main::i@16|)
(define-fun .5299 () (_ BitVec 32) (bvshl .5294 .43))
(define-fun .5304 () (_ BitVec 32) (bvadd .37 .5294))
(define-fun .6205 () Bool (= .5304 .6204))
(define-fun .9029 () Bool (bvslt .5294 .18))
(define-fun .9054 () (_ BitVec 32) (bvadd .167 .5299))
(define-fun .9059 () (_ BitVec 32) (bvadd .25 .5299))
(define-fun .9072 () (_ BitVec 32) (bvadd .277 .5299))
(define-fun .10192 () (_ BitVec 32) |main::x@11|)
(define-fun .10197 () (_ BitVec 32) |main::y@11|)
(define-fun .10201 () (_ BitVec 32) (bvshl .10192 .43))
(define-fun .10202 () (_ BitVec 32) (bvadd .387 .10201))
(define-fun .10205 () (_ BitVec 32) (bvshl .10197 .43))
(define-fun .10206 () (_ BitVec 32) (bvadd .387 .10205))
(define-fun .25880 () (_ BitVec 32) (select .24842 .9054))
(define-fun .25881 () Bool (= .10192 .25880))
(define-fun .25882 () Bool (and .9029 .25881))
(define-fun .25883 () (_ BitVec 32) (select .24842 .9059))
(define-fun .25884 () Bool (= .10197 .25883))
(define-fun .25885 () Bool (and .25882 .25884))
(define-fun .25886 () (_ BitVec 32) (select .24842 .10202))
(define-fun .25887 () (_ BitVec 32) (select .24842 .10206))
(define-fun .25888 () (_ BitVec 32) (select .24842 .9072))
(define-fun .25889 () (_ BitVec 32) (bvadd .25887 .25888))
(define-fun .25890 () Bool (bvslt .25889 .25886))
(define-fun .25893 () Bool (not .25890))
(define-fun .25894 () Bool (and .25885 .25893))
(define-fun .25895 () Bool (and .6205 .25894))
(assert (! .25895 :interpolation-group .g10))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g10))
(declare-fun |main::i@8| () (_ BitVec 32))
(declare-fun *int@6 () (Array (_ BitVec 32) (_ BitVec 32)))
(define-fun .733 () Bool (bvslt .724 .14))
(define-fun .738 () (_ BitVec 32) (bvshl .724 .43))
(define-fun .739 () (_ BitVec 32) (bvadd .387 .738))
(define-fun .871 () (_ BitVec 32) (bvadd .37 .724))
(define-fun .872 () (_ BitVec 32) |main::i@8|)
(define-fun .873 () Bool (= .871 .872))
(define-fun .2535 () Bool (= .21 .724))
(define-fun .2614 () Bool (not .2535))
(define-fun .3877 () Bool (and .733 .2535))
(define-fun .3878 () Bool (and .733 .2614))
(define-fun .3879 () (Array (_ BitVec 32) (_ BitVec 32)) *int@6)
(define-fun .3880 () (Array (_ BitVec 32) (_ BitVec 32)) (store .2522 .739 .11))
(define-fun .3881 () Bool (= .3879 .3880))
(define-fun .3882 () Bool (and .3878 .3881))
(define-fun .3883 () (Array (_ BitVec 32) (_ BitVec 32)) (store .2522 .739 .8))
(define-fun .3884 () Bool (= .3879 .3883))
(define-fun .3885 () Bool (and .3877 .3884))
(define-fun .3886 () Bool (or .3882 .3885))
(define-fun .3887 () Bool (and .873 .3886))
(assert (! .3887 :interpolation-group .g11))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g11))
(declare-fun |main::i@15| () (_ BitVec 32))
(declare-fun |main::x@10| () (_ BitVec 32))
(declare-fun |main::y@10| () (_ BitVec 32))
(define-fun .4384 () (_ BitVec 32) |main::i@15|)
(define-fun .4389 () (_ BitVec 32) (bvshl .4384 .43))
(define-fun .4394 () (_ BitVec 32) (bvadd .37 .4384))
(define-fun .5295 () Bool (= .4394 .5294))
(define-fun .8911 () Bool (bvslt .4384 .18))
(define-fun .8936 () (_ BitVec 32) (bvadd .167 .4389))
(define-fun .8941 () (_ BitVec 32) (bvadd .25 .4389))
(define-fun .8954 () (_ BitVec 32) (bvadd .277 .4389))
(define-fun .10063 () (_ BitVec 32) |main::x@10|)
(define-fun .10068 () (_ BitVec 32) |main::y@10|)
(define-fun .10072 () (_ BitVec 32) (bvshl .10063 .43))
(define-fun .10073 () (_ BitVec 32) (bvadd .387 .10072))
(define-fun .10076 () (_ BitVec 32) (bvshl .10068 .43))
(define-fun .10077 () (_ BitVec 32) (bvadd .387 .10076))
(define-fun .25669 () (_ BitVec 32) (select .24842 .8936))
(define-fun .25670 () Bool (= .10063 .25669))
(define-fun .25671 () Bool (and .8911 .25670))
(define-fun .25672 () (_ BitVec 32) (select .24842 .8941))
(define-fun .25673 () Bool (= .10068 .25672))
(define-fun .25674 () Bool (and .25671 .25673))
(define-fun .25675 () (_ BitVec 32) (select .24842 .10073))
(define-fun .25676 () (_ BitVec 32) (select .24842 .10077))
(define-fun .25677 () (_ BitVec 32) (select .24842 .8954))
(define-fun .25678 () (_ BitVec 32) (bvadd .25676 .25677))
(define-fun .25679 () Bool (bvslt .25678 .25675))
(define-fun .25682 () Bool (not .25679))
(define-fun .25683 () Bool (and .25674 .25682))
(define-fun .25684 () Bool (and .5295 .25683))
(assert (! .25684 :interpolation-group .g12))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g12))
(declare-fun |main::i@9| () (_ BitVec 32))
(define-fun .897 () Bool (bvslt .872 .14))
(define-fun .899 () Bool (not .897))
(define-fun .1078 () (_ BitVec 32) |main::i@9|)
(define-fun .1082 () Bool (= .1078 .8))
(define-fun .2635 () Bool (and .899 .1082))
(assert (! .2635 :interpolation-group .g13))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g13))
(declare-fun |main::i@14| () (_ BitVec 32))
(declare-fun |main::x@9| () (_ BitVec 32))
(declare-fun |main::y@9| () (_ BitVec 32))
(define-fun .3477 () (_ BitVec 32) |main::i@14|)
(define-fun .3482 () (_ BitVec 32) (bvshl .3477 .43))
(define-fun .3487 () (_ BitVec 32) (bvadd .37 .3477))
(define-fun .4385 () Bool (= .3487 .4384))
(define-fun .8072 () Bool (bvslt .3477 .18))
(define-fun .8097 () (_ BitVec 32) (bvadd .167 .3482))
(define-fun .8102 () (_ BitVec 32) (bvadd .25 .3482))
(define-fun .8115 () (_ BitVec 32) (bvadd .277 .3482))
(define-fun .9056 () (_ BitVec 32) |main::x@9|)
(define-fun .9061 () (_ BitVec 32) |main::y@9|)
(define-fun .9065 () (_ BitVec 32) (bvshl .9056 .43))
(define-fun .9066 () (_ BitVec 32) (bvadd .387 .9065))
(define-fun .9069 () (_ BitVec 32) (bvshl .9061 .43))
(define-fun .9070 () (_ BitVec 32) (bvadd .387 .9069))
(define-fun .25517 () (_ BitVec 32) (select .24842 .8097))
(define-fun .25518 () Bool (= .9056 .25517))
(define-fun .25519 () Bool (and .8072 .25518))
(define-fun .25520 () (_ BitVec 32) (select .24842 .8102))
(define-fun .25521 () Bool (= .9061 .25520))
(define-fun .25522 () Bool (and .25519 .25521))
(define-fun .25523 () (_ BitVec 32) (select .24842 .9066))
(define-fun .25524 () (_ BitVec 32) (select .24842 .9070))
(define-fun .25525 () (_ BitVec 32) (select .24842 .8115))
(define-fun .25526 () (_ BitVec 32) (bvadd .25524 .25525))
(define-fun .25527 () Bool (bvslt .25526 .25523))
(define-fun .25530 () Bool (not .25527))
(define-fun .25531 () Bool (and .25522 .25530))
(define-fun .25532 () Bool (and .4385 .25531))
(assert (! .25532 :interpolation-group .g14))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g14))
(declare-fun |main::j@3| () (_ BitVec 32))
(define-fun .1101 () Bool (bvslt .1078 .14))
(define-fun .6416 () (_ BitVec 32) |main::j@3|)
(define-fun .6417 () Bool (= .6416 .8))
(define-fun .6418 () Bool (and .1101 .6417))
(assert (! .6418 :interpolation-group .g15))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g15))
(declare-fun |main::i@13| () (_ BitVec 32))
(declare-fun |main::x@8| () (_ BitVec 32))
(declare-fun |main::y@8| () (_ BitVec 32))
(define-fun .2838 () (_ BitVec 32) |main::i@13|)
(define-fun .2843 () (_ BitVec 32) (bvshl .2838 .43))
(define-fun .2848 () (_ BitVec 32) (bvadd .37 .2838))
(define-fun .3478 () Bool (= .2848 .3477))
(define-fun .7954 () Bool (bvslt .2838 .18))
(define-fun .7983 () (_ BitVec 32) (bvadd .167 .2843))
(define-fun .7988 () (_ BitVec 32) (bvadd .25 .2843))
(define-fun .8001 () (_ BitVec 32) (bvadd .277 .2843))
(define-fun .8938 () (_ BitVec 32) |main::x@8|)
(define-fun .8943 () (_ BitVec 32) |main::y@8|)
(define-fun .8947 () (_ BitVec 32) (bvshl .8938 .43))
(define-fun .8948 () (_ BitVec 32) (bvadd .387 .8947))
(define-fun .8951 () (_ BitVec 32) (bvshl .8943 .43))
(define-fun .8952 () (_ BitVec 32) (bvadd .387 .8951))
(define-fun .25357 () (_ BitVec 32) (select .24842 .7983))
(define-fun .25358 () Bool (= .8938 .25357))
(define-fun .25359 () Bool (and .7954 .25358))
(define-fun .25360 () (_ BitVec 32) (select .24842 .7988))
(define-fun .25361 () Bool (= .8943 .25360))
(define-fun .25362 () Bool (and .25359 .25361))
(define-fun .25363 () (_ BitVec 32) (select .24842 .8948))
(define-fun .25364 () (_ BitVec 32) (select .24842 .8952))
(define-fun .25365 () (_ BitVec 32) (select .24842 .8001))
(define-fun .25366 () (_ BitVec 32) (bvadd .25364 .25365))
(define-fun .25367 () Bool (bvslt .25366 .25363))
(define-fun .25370 () Bool (not .25367))
(define-fun .25371 () Bool (and .25362 .25370))
(define-fun .25372 () Bool (and .3478 .25371))
(assert (! .25372 :interpolation-group .g16))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g16))
(declare-fun |main::x@3| () (_ BitVec 32))
(declare-fun |main::y@3| () (_ BitVec 32))
(declare-fun *int@7 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun |main::j@4| () (_ BitVec 32))
(define-fun .6350 () (_ BitVec 32) |main::x@3|)
(define-fun .6355 () (_ BitVec 32) |main::y@3|)
(define-fun .6359 () (_ BitVec 32) (bvshl .6350 .43))
(define-fun .6360 () (_ BitVec 32) (bvadd .387 .6359))
(define-fun .6361 () (_ BitVec 32) (select .3879 .6360))
(define-fun .6363 () (_ BitVec 32) (bvshl .6355 .43))
(define-fun .6364 () (_ BitVec 32) (bvadd .387 .6363))
(define-fun .6365 () (_ BitVec 32) (select .3879 .6364))
(define-fun .6420 () Bool (bvslt .6416 .18))
(define-fun .11336 () (_ BitVec 32) (bvshl .6416 .43))
(define-fun .11337 () (_ BitVec 32) (bvadd .167 .11336))
(define-fun .11338 () (_ BitVec 32) (select .3879 .11337))
(define-fun .11339 () Bool (= .6350 .11338))
(define-fun .11340 () Bool (and .6420 .11339))
(define-fun .11341 () (_ BitVec 32) (bvadd .25 .11336))
(define-fun .11342 () (_ BitVec 32) (select .3879 .11341))
(define-fun .11343 () Bool (= .6355 .11342))
(define-fun .11344 () Bool (and .11340 .11343))
(define-fun .11345 () (_ BitVec 32) (bvadd .277 .11336))
(define-fun .11346 () (_ BitVec 32) (select .3879 .11345))
(define-fun .11347 () (_ BitVec 32) (bvadd .6365 .11346))
(define-fun .11348 () Bool (bvslt .11347 .6361))
(define-fun .11350 () Bool (and .11344 .11348))
(define-fun .11351 () Bool (not .11348))
(define-fun .11352 () Bool (and .11344 .11351))
(define-fun .11353 () (Array (_ BitVec 32) (_ BitVec 32)) *int@7)
(define-fun .11354 () (Array (_ BitVec 32) (_ BitVec 32)) (store .3879 .6360 .11347))
(define-fun .11355 () Bool (= .11353 .11354))
(define-fun .11356 () Bool (and .11350 .11355))
(define-fun .11357 () Bool (= .3879 .11353))
(define-fun .11358 () Bool (and .11352 .11357))
(define-fun .11359 () Bool (or .11356 .11358))
(define-fun .11361 () (_ BitVec 32) (bvadd .37 .6416))
(define-fun .11362 () (_ BitVec 32) |main::j@4|)
(define-fun .11363 () Bool (= .11361 .11362))
(define-fun .11364 () Bool (and .11359 .11363))
(assert (! .11364 :interpolation-group .g17))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g17))
(declare-fun |main::i@12| () (_ BitVec 32))
(declare-fun |main::x@7| () (_ BitVec 32))
(declare-fun |main::y@7| () (_ BitVec 32))
(define-fun .2253 () (_ BitVec 32) |main::i@12|)
(define-fun .2258 () (_ BitVec 32) (bvshl .2253 .43))
(define-fun .2263 () (_ BitVec 32) (bvadd .37 .2253))
(define-fun .2839 () Bool (= .2263 .2838))
(define-fun .7268 () Bool (bvslt .2253 .18))
(define-fun .7295 () (_ BitVec 32) (bvadd .167 .2258))
(define-fun .7300 () (_ BitVec 32) (bvadd .25 .2258))
(define-fun .7313 () (_ BitVec 32) (bvadd .277 .2258))
(define-fun .8099 () (_ BitVec 32) |main::x@7|)
(define-fun .8104 () (_ BitVec 32) |main::y@7|)
(define-fun .8108 () (_ BitVec 32) (bvshl .8099 .43))
(define-fun .8109 () (_ BitVec 32) (bvadd .387 .8108))
(define-fun .8112 () (_ BitVec 32) (bvshl .8104 .43))
(define-fun .8113 () (_ BitVec 32) (bvadd .387 .8112))
(define-fun .25192 () (_ BitVec 32) (select .24842 .7295))
(define-fun .25193 () Bool (= .8099 .25192))
(define-fun .25194 () Bool (and .7268 .25193))
(define-fun .25195 () (_ BitVec 32) (select .24842 .7300))
(define-fun .25196 () Bool (= .8104 .25195))
(define-fun .25197 () Bool (and .25194 .25196))
(define-fun .25198 () (_ BitVec 32) (select .24842 .8109))
(define-fun .25199 () (_ BitVec 32) (select .24842 .8113))
(define-fun .25200 () (_ BitVec 32) (select .24842 .7313))
(define-fun .25201 () (_ BitVec 32) (bvadd .25199 .25200))
(define-fun .25202 () Bool (bvslt .25201 .25198))
(define-fun .25205 () Bool (not .25202))
(define-fun .25206 () Bool (and .25197 .25205))
(define-fun .25207 () Bool (and .2839 .25206))
(assert (! .25207 :interpolation-group .g18))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g18))
(declare-fun |main::x@4| () (_ BitVec 32))
(declare-fun |main::y@4| () (_ BitVec 32))
(declare-fun *int@8 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun |main::j@5| () (_ BitVec 32))
(define-fun .7203 () (_ BitVec 32) |main::x@4|)
(define-fun .7208 () (_ BitVec 32) |main::y@4|)
(define-fun .7212 () (_ BitVec 32) (bvshl .7203 .43))
(define-fun .7213 () (_ BitVec 32) (bvadd .387 .7212))
(define-fun .7216 () (_ BitVec 32) (bvshl .7208 .43))
(define-fun .7217 () (_ BitVec 32) (bvadd .387 .7216))
(define-fun .11407 () Bool (bvslt .11362 .18))
(define-fun .11532 () (_ BitVec 32) (select .11353 .7213))
(define-fun .11533 () (_ BitVec 32) (select .11353 .7217))
(define-fun .19122 () (_ BitVec 32) (bvshl .11362 .43))
(define-fun .19123 () (_ BitVec 32) (bvadd .167 .19122))
(define-fun .19124 () (_ BitVec 32) (select .11353 .19123))
(define-fun .19125 () Bool (= .7203 .19124))
(define-fun .19126 () Bool (and .11407 .19125))
(define-fun .19127 () (_ BitVec 32) (bvadd .25 .19122))
(define-fun .19128 () (_ BitVec 32) (select .11353 .19127))
(define-fun .19129 () Bool (= .7208 .19128))
(define-fun .19130 () Bool (and .19126 .19129))
(define-fun .19131 () (_ BitVec 32) (bvadd .277 .19122))
(define-fun .19132 () (_ BitVec 32) (select .11353 .19131))
(define-fun .19133 () (_ BitVec 32) (bvadd .11533 .19132))
(define-fun .19134 () Bool (bvslt .19133 .11532))
(define-fun .19136 () Bool (and .19130 .19134))
(define-fun .19137 () Bool (not .19134))
(define-fun .19138 () Bool (and .19130 .19137))
(define-fun .19139 () (Array (_ BitVec 32) (_ BitVec 32)) *int@8)
(define-fun .19140 () (Array (_ BitVec 32) (_ BitVec 32)) (store .11353 .7213 .19133))
(define-fun .19141 () Bool (= .19139 .19140))
(define-fun .19142 () Bool (and .19136 .19141))
(define-fun .19143 () Bool (= .11353 .19139))
(define-fun .19144 () Bool (and .19138 .19143))
(define-fun .19145 () Bool (or .19142 .19144))
(define-fun .19147 () (_ BitVec 32) (bvadd .37 .11362))
(define-fun .19148 () (_ BitVec 32) |main::j@5|)
(define-fun .19149 () Bool (= .19147 .19148))
(define-fun .19150 () Bool (and .19145 .19149))
(assert (! .19150 :interpolation-group .g19))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g19))
(declare-fun |main::i@11| () (_ BitVec 32))
(declare-fun |main::x@6| () (_ BitVec 32))
(declare-fun |main::y@6| () (_ BitVec 32))
(define-fun .1827 () (_ BitVec 32) |main::i@11|)
(define-fun .1832 () (_ BitVec 32) (bvshl .1827 .43))
(define-fun .1837 () (_ BitVec 32) (bvadd .37 .1827))
(define-fun .2254 () Bool (= .1837 .2253))
(define-fun .6431 () Bool (bvslt .1827 .18))
(define-fun .7201 () (_ BitVec 32) (bvadd .167 .1832))
(define-fun .7206 () (_ BitVec 32) (bvadd .25 .1832))
(define-fun .7219 () (_ BitVec 32) (bvadd .277 .1832))
(define-fun .7985 () (_ BitVec 32) |main::x@6|)
(define-fun .7990 () (_ BitVec 32) |main::y@6|)
(define-fun .7994 () (_ BitVec 32) (bvshl .7985 .43))
(define-fun .7995 () (_ BitVec 32) (bvadd .387 .7994))
(define-fun .7998 () (_ BitVec 32) (bvshl .7990 .43))
(define-fun .7999 () (_ BitVec 32) (bvadd .387 .7998))
(define-fun .25019 () (_ BitVec 32) (select .24842 .7201))
(define-fun .25020 () Bool (= .7985 .25019))
(define-fun .25021 () Bool (and .6431 .25020))
(define-fun .25022 () (_ BitVec 32) (select .24842 .7206))
(define-fun .25023 () Bool (= .7990 .25022))
(define-fun .25024 () Bool (and .25021 .25023))
(define-fun .25025 () (_ BitVec 32) (select .24842 .7995))
(define-fun .25026 () (_ BitVec 32) (select .24842 .7999))
(define-fun .25027 () (_ BitVec 32) (select .24842 .7219))
(define-fun .25028 () (_ BitVec 32) (bvadd .25026 .25027))
(define-fun .25029 () Bool (bvslt .25028 .25025))
(define-fun .25032 () Bool (not .25029))
(define-fun .25033 () Bool (and .25024 .25032))
(define-fun .25034 () Bool (and .2254 .25033))
(assert (! .25034 :interpolation-group .g20))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g20))
(declare-fun |main::x@5| () (_ BitVec 32))
(declare-fun |main::y@5| () (_ BitVec 32))
(declare-fun |main::j@6| () (_ BitVec 32))
(define-fun .7297 () (_ BitVec 32) |main::x@5|)
(define-fun .7302 () (_ BitVec 32) |main::y@5|)
(define-fun .7306 () (_ BitVec 32) (bvshl .7297 .43))
(define-fun .7307 () (_ BitVec 32) (bvadd .387 .7306))
(define-fun .7310 () (_ BitVec 32) (bvshl .7302 .43))
(define-fun .7311 () (_ BitVec 32) (bvadd .387 .7310))
(define-fun .19192 () Bool (bvslt .19148 .18))
(define-fun .19319 () (_ BitVec 32) (select .19139 .7307))
(define-fun .19320 () (_ BitVec 32) (select .19139 .7311))
(define-fun .24825 () (_ BitVec 32) (bvshl .19148 .43))
(define-fun .24826 () (_ BitVec 32) (bvadd .167 .24825))
(define-fun .24827 () (_ BitVec 32) (select .19139 .24826))
(define-fun .24828 () Bool (= .7297 .24827))
(define-fun .24829 () Bool (and .19192 .24828))
(define-fun .24830 () (_ BitVec 32) (bvadd .25 .24825))
(define-fun .24831 () (_ BitVec 32) (select .19139 .24830))
(define-fun .24832 () Bool (= .7302 .24831))
(define-fun .24833 () Bool (and .24829 .24832))
(define-fun .24834 () (_ BitVec 32) (bvadd .277 .24825))
(define-fun .24835 () (_ BitVec 32) (select .19139 .24834))
(define-fun .24836 () (_ BitVec 32) (bvadd .19320 .24835))
(define-fun .24837 () Bool (bvslt .24836 .19319))
(define-fun .24839 () Bool (and .24833 .24837))
(define-fun .24840 () Bool (not .24837))
(define-fun .24841 () Bool (and .24833 .24840))
(define-fun .24843 () (Array (_ BitVec 32) (_ BitVec 32)) (store .19139 .7307 .24836))
(define-fun .24844 () Bool (= .24842 .24843))
(define-fun .24845 () Bool (and .24839 .24844))
(define-fun .24846 () Bool (= .19139 .24842))
(define-fun .24847 () Bool (and .24841 .24846))
(define-fun .24848 () Bool (or .24845 .24847))
(define-fun .24850 () (_ BitVec 32) (bvadd .37 .19148))
(define-fun .24851 () (_ BitVec 32) |main::j@6|)
(define-fun .24852 () Bool (= .24850 .24851))
(define-fun .24853 () Bool (and .24848 .24852))
(assert (! .24853 :interpolation-group .g21))
(check-sat)
(push 1)
(assert (! true :interpolation-group .g21))
(declare-fun |main::i@10| () (_ BitVec 32))
(define-fun .1401 () (_ BitVec 32) |main::i@10|)
(define-fun .1454 () Bool (bvslt .1401 .14))
(define-fun .1456 () Bool (not .1454))
(define-fun .1831 () Bool (= .1827 .8))
(define-fun .6424 () Bool (and .1456 .1831))
(assert (! .6424 :interpolation-group .g22))
(push 1)
(assert (! true :interpolation-group .g22))
(define-fun .1370 () (_ BitVec 32) (bvadd .37 .1078))
(define-fun .1402 () Bool (= .1370 .1401))
(define-fun .24898 () Bool (bvslt .24851 .18))
(define-fun .24900 () Bool (not .24898))
(define-fun .24901 () Bool (and .1402 .24900))
(assert (! .24901 :interpolation-group .g23))
(check-sat)
(get-interpolant (.g1))
baierd commented 4 years ago

I made a C program illustrating the same example, but either i made a mistake or (more likely) the error is catched by the assertion that fails when you run it. (If you copy it, its the assert(!MSAT_ERROR_TERM(interpolant)); in line 278 that fails)

However removing the assert results in a SegFault and we don't have that assert or check in JavaSMT (if i did not miss it, its late). If this is indeed the case i will test/fix this tomorrow so that the very least JavaSMT doesn't crash anymore.

C example code(change PATH/TO/MATHSAT and filename accordingly):

//Example for failing interpolation resulting in a SigSev

/* The notes here are for me (dBaier) and shouldn't be followed if you know what you are doing ;D
 * Export path to lib first: export LD_LIBRARY_PATH=/PATH/TO/MATHSAT/
 * to compile: 
 * gcc example_sigsev_interpolation.c -I/PATH/TO/MATHSAT/mathsat-5.6.4-linux-x86_64-reentrant/include -L/PATH/TO/MATHSAT/mathsat-5.6.4-linux-x86_64-reentrant/lib -lmathsat -lgmpxx -lgmp -lstdc++ -o example_sigsev_interpolation
 */

#include <stdio.h>
#include <assert.h>
#include <stdlib.h>
#include "mathsat.h"

/* Declare the Formulas we will use. 
 * Each Formula corrosponds to a interpolation group with the same number!
 */

static char* formula0 = "(declare-fun |main::nodecount@2| () (_ BitVec 32))(declare-fun |__ADDRESS_OF_main::distance@| () (_ BitVec 32))(declare-fun |__VERIFIER_assert::cond@2| () (_ BitVec 32))(declare-fun |main::i@21| () (_ BitVec 32))(declare-fun *int@9 () (Array (_ BitVec 32) (_ BitVec 32)))(assert (and (= |__VERIFIER_assert::cond@2| (_ bv0 32)) (and (bvslt |main::i@21| |main::nodecount@2|) (= |__VERIFIER_assert::cond@2| (ite (not (= ((_ extract 31 31) (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::i@21| (_ bv2 32))))) (_ bv1 1))) (_ bv1 32) (_ bv0 32))))))";
static char* formula1 = "(declare-fun INFINITY@2 () (_ BitVec 32))(declare-fun |main::edgecount@2| () (_ BitVec 32))(declare-fun |main::source@2| () (_ BitVec 32))(declare-fun |__ADDRESS_OF_main::Source@| () (_ BitVec 32))(declare-fun *int@1 () (Array (_ BitVec 32) (_ BitVec 32)))(declare-fun |__ADDRESS_OF_main::Dest@| () (_ BitVec 32))(declare-fun |__ADDRESS_OF_main::Weight@| () (_ BitVec 32))(declare-fun |main::i@3| () (_ BitVec 32))(assert (and (and (and (and (and (and (and (and (= INFINITY@2 (_ bv899 32)) (= |main::nodecount@2| (_ bv5 32))) (= |main::edgecount@2| (_ bv20 32))) (= |main::source@2| (_ bv0 32))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= *int@1 (store *int@1 |__ADDRESS_OF_main::Source@| (_ bv0 32))) (= *int@1 (store *int@1 (bvadd (_ bv4 32) |__ADDRESS_OF_main::Source@|) (_ bv4 32)))) (= *int@1 (store *int@1 (bvadd (_ bv8 32) |__ADDRESS_OF_main::Source@|) (_ bv1 32)))) (= *int@1 (store *int@1 (bvadd (_ bv12 32) |__ADDRESS_OF_main::Source@|) (_ bv1 32)))) (= *int@1 (store *int@1 (bvadd (_ bv16 32) |__ADDRESS_OF_main::Source@|) (_ bv0 32)))) (= *int@1 (store *int@1 (bvadd (_ bv20 32) |__ADDRESS_OF_main::Source@|) (_ bv0 32)))) (= *int@1 (store *int@1 (bvadd (_ bv24 32) |__ADDRESS_OF_main::Source@|) (_ bv1 32)))) (= *int@1 (store *int@1 (bvadd (_ bv28 32) |__ADDRESS_OF_main::Source@|) (_ bv3 32)))) (= *int@1 (store *int@1 (bvadd (_ bv32 32) |__ADDRESS_OF_main::Source@|) (_ bv4 32)))) (= *int@1 (store *int@1 (bvadd (_ bv36 32) |__ADDRESS_OF_main::Source@|) (_ bv4 32)))) (= *int@1 (store *int@1 (bvadd (_ bv40 32) |__ADDRESS_OF_main::Source@|) (_ bv2 32)))) (= *int@1 (store *int@1 (bvadd (_ bv44 32) |__ADDRESS_OF_main::Source@|) (_ bv2 32)))) (= *int@1 (store *int@1 (bvadd (_ bv48 32) |__ADDRESS_OF_main::Source@|) (_ bv3 32)))) (= *int@1 (store *int@1 (bvadd (_ bv52 32) |__ADDRESS_OF_main::Source@|) (_ bv0 32)))) (= *int@1 (store *int@1 (bvadd (_ bv56 32) |__ADDRESS_OF_main::Source@|) (_ bv0 32)))) (= *int@1 (store *int@1 (bvadd (_ bv60 32) |__ADDRESS_OF_main::Source@|) (_ bv3 32)))) (= *int@1 (store *int@1 (bvadd (_ bv64 32) |__ADDRESS_OF_main::Source@|) (_ bv1 32)))) (= *int@1 (store *int@1 (bvadd (_ bv68 32) |__ADDRESS_OF_main::Source@|) (_ bv2 32)))) (= *int@1 (store *int@1 (bvadd (_ bv72 32) |__ADDRESS_OF_main::Source@|) (_ bv2 32)))) (= *int@1 (store *int@1 (bvadd (_ bv76 32) |__ADDRESS_OF_main::Source@|) (_ bv3 32)))) (and (bvslt (_ bv0 32) (bvadd (_ bv80 32) |__ADDRESS_OF_main::Source@|)) (and (bvslt (_ bv0 32) |__ADDRESS_OF_main::Source@|) (= (bvurem |__ADDRESS_OF_main::Source@| (_ bv4 32)) (_ bv0 32)))))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= *int@1 (store *int@1 |__ADDRESS_OF_main::Dest@| (_ bv1 32))) (= *int@1 (store *int@1 (bvadd (_ bv4 32) |__ADDRESS_OF_main::Dest@|) (_ bv3 32)))) (= *int@1 (store *int@1 (bvadd (_ bv8 32) |__ADDRESS_OF_main::Dest@|) (_ bv4 32)))) (= *int@1 (store *int@1 (bvadd (_ bv12 32) |__ADDRESS_OF_main::Dest@|) (_ bv1 32)))) (= *int@1 (store *int@1 (bvadd (_ bv16 32) |__ADDRESS_OF_main::Dest@|) (_ bv1 32)))) (= *int@1 (store *int@1 (bvadd (_ bv20 32) |__ADDRESS_OF_main::Dest@|) (_ bv4 32)))) (= *int@1 (store *int@1 (bvadd (_ bv24 32) |__ADDRESS_OF_main::Dest@|) (_ bv3 32)))) (= *int@1 (store *int@1 (bvadd (_ bv28 32) |__ADDRESS_OF_main::Dest@|) (_ bv4 32)))) (= *int@1 (store *int@1 (bvadd (_ bv32 32) |__ADDRESS_OF_main::Dest@|) (_ bv3 32)))) (= *int@1 (store *int@1 (bvadd (_ bv36 32) |__ADDRESS_OF_main::Dest@|) (_ bv0 32)))) (= *int@1 (store *int@1 (bvadd (_ bv40 32) |__ADDRESS_OF_main::Dest@|) (_ bv0 32)))) (= *int@1 (store *int@1 (bvadd (_ bv44 32) |__ADDRESS_OF_main::Dest@|) (_ bv0 32)))) (= *int@1 (store *int@1 (bvadd (_ bv48 32) |__ADDRESS_OF_main::Dest@|) (_ bv0 32)))) (= *int@1 (store *int@1 (bvadd (_ bv52 32) |__ADDRESS_OF_main::Dest@|) (_ bv2 32)))) (= *int@1 (store *int@1 (bvadd (_ bv56 32) |__ADDRESS_OF_main::Dest@|) (_ bv3 32)))) (= *int@1 (store *int@1 (bvadd (_ bv60 32) |__ADDRESS_OF_main::Dest@|) (_ bv0 32)))) (= *int@1 (store *int@1 (bvadd (_ bv64 32) |__ADDRESS_OF_main::Dest@|) (_ bv2 32)))) (= *int@1 (store *int@1 (bvadd (_ bv68 32) |__ADDRESS_OF_main::Dest@|) (_ bv1 32)))) (= *int@1 (store *int@1 (bvadd (_ bv72 32) |__ADDRESS_OF_main::Dest@|) (_ bv0 32)))) (= *int@1 (store *int@1 (bvadd (_ bv76 32) |__ADDRESS_OF_main::Dest@|) (_ bv4 32)))) (and (bvslt (_ bv0 32) (bvadd (_ bv80 32) |__ADDRESS_OF_main::Dest@|)) (and (bvslt (bvadd (_ bv80 32) |__ADDRESS_OF_main::Source@|) |__ADDRESS_OF_main::Dest@|) (= (bvurem |__ADDRESS_OF_main::Dest@| (_ bv4 32)) (_ bv0 32)))))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= *int@1 (store *int@1 |__ADDRESS_OF_main::Weight@| (_ bv0 32))) (= *int@1 (store *int@1 (bvadd (_ bv4 32) |__ADDRESS_OF_main::Weight@|) (_ bv1 32)))) (= *int@1 (store *int@1 (bvadd (_ bv8 32) |__ADDRESS_OF_main::Weight@|) (_ bv2 32)))) (= *int@1 (store *int@1 (bvadd (_ bv12 32) |__ADDRESS_OF_main::Weight@|) (_ bv3 32)))) (= *int@1 (store *int@1 (bvadd (_ bv16 32) |__ADDRESS_OF_main::Weight@|) (_ bv4 32)))) (= *int@1 (store *int@1 (bvadd (_ bv20 32) |__ADDRESS_OF_main::Weight@|) (_ bv5 32)))) (= *int@1 (store *int@1 (bvadd (_ bv24 32) |__ADDRESS_OF_main::Weight@|) (_ bv6 32)))) (= *int@1 (store *int@1 (bvadd (_ bv28 32) |__ADDRESS_OF_main::Weight@|) (_ bv7 32)))) (= *int@1 (store *int@1 (bvadd (_ bv32 32) |__ADDRESS_OF_main::Weight@|) (_ bv8 32)))) (= *int@1 (store *int@1 (bvadd (_ bv36 32) |__ADDRESS_OF_main::Weight@|) (_ bv9 32)))) (= *int@1 (store *int@1 (bvadd (_ bv40 32) |__ADDRESS_OF_main::Weight@|) (_ bv10 32)))) (= *int@1 (store *int@1 (bvadd (_ bv44 32) |__ADDRESS_OF_main::Weight@|) (_ bv11 32)))) (= *int@1 (store *int@1 (bvadd (_ bv48 32) |__ADDRESS_OF_main::Weight@|) (_ bv12 32)))) (= *int@1 (store *int@1 (bvadd (_ bv52 32) |__ADDRESS_OF_main::Weight@|) (_ bv13 32)))) (= *int@1 (store *int@1 (bvadd (_ bv56 32) |__ADDRESS_OF_main::Weight@|) (_ bv14 32)))) (= *int@1 (store *int@1 (bvadd (_ bv60 32) |__ADDRESS_OF_main::Weight@|) (_ bv15 32)))) (= *int@1 (store *int@1 (bvadd (_ bv64 32) |__ADDRESS_OF_main::Weight@|) (_ bv16 32)))) (= *int@1 (store *int@1 (bvadd (_ bv68 32) |__ADDRESS_OF_main::Weight@|) (_ bv17 32)))) (= *int@1 (store *int@1 (bvadd (_ bv72 32) |__ADDRESS_OF_main::Weight@|) (_ bv18 32)))) (= *int@1 (store *int@1 (bvadd (_ bv76 32) |__ADDRESS_OF_main::Weight@|) (_ bv19 32)))) (and (bvslt (_ bv0 32) (bvadd (_ bv80 32) |__ADDRESS_OF_main::Weight@|)) (and (bvslt (bvadd (_ bv80 32) |__ADDRESS_OF_main::Dest@|) |__ADDRESS_OF_main::Weight@|) (= (bvurem |__ADDRESS_OF_main::Weight@| (_ bv4 32)) (_ bv0 32)))))) (and (bvslt (_ bv0 32) (bvadd (_ bv20 32) |__ADDRESS_OF_main::distance@|)) (and (bvslt (bvadd (_ bv80 32) |__ADDRESS_OF_main::Weight@|) |__ADDRESS_OF_main::distance@|) (= (bvurem |__ADDRESS_OF_main::distance@| (_ bv4 32)) (_ bv0 32))))) (= |main::i@3| (_ bv0 32))))";
static char* formula2 = "(declare-fun |main::i@20| () (_ BitVec 32))(assert (and (= |main::i@21| (_ bv0 32)) (not (bvslt |main::i@20| |main::edgecount@2|))))";
static char* formula3 = "(declare-fun |main::i@4| () (_ BitVec 32))(declare-fun *int@2 () (Array (_ BitVec 32) (_ BitVec 32)))(assert (and (or (and (and (bvslt |main::i@3| |main::nodecount@2|) (not (= |main::source@2| |main::i@3|))) (= *int@2 (store *int@1 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::i@3| (_ bv2 32))) INFINITY@2))) (and (and (bvslt |main::i@3| |main::nodecount@2|) (= |main::source@2| |main::i@3|)) (= *int@2 (store *int@1 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::i@3| (_ bv2 32))) (_ bv0 32))))) (= |main::i@4| (bvadd (_ bv1 32) |main::i@3|))))";
static char* formula4 = "(declare-fun |main::i@19| () (_ BitVec 32))(declare-fun |main::x@14| () (_ BitVec 32))(declare-fun |main::y@14| () (_ BitVec 32))(assert (and (= (bvadd (_ bv1 32) |main::i@19|) |main::i@20|) (and (and (and (bvslt |main::i@19| |main::edgecount@2|) (= |main::x@14| (select *int@9 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::i@19| (_ bv2 32)))))) (= |main::y@14| (select *int@9 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::i@19| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@14| (_ bv2 32)))) (select *int@9 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::i@19| (_ bv2 32))))) (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@14| (_ bv2 32)))))))))";
static char* formula5 = "(declare-fun |main::i@5| () (_ BitVec 32))(declare-fun *int@3 () (Array (_ BitVec 32) (_ BitVec 32)))(assert (and (or (and (and (bvslt |main::i@4| |main::nodecount@2|) (not (= |main::source@2| |main::i@4|))) (= *int@3 (store *int@2 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::i@4| (_ bv2 32))) INFINITY@2))) (and (and (bvslt |main::i@4| |main::nodecount@2|) (= |main::source@2| |main::i@4|)) (= *int@3 (store *int@2 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::i@4| (_ bv2 32))) (_ bv0 32))))) (= |main::i@5| (bvadd (_ bv1 32) |main::i@4|))))";
static char* formula6 = "(declare-fun |main::i@18| () (_ BitVec 32))(declare-fun |main::x@13| () (_ BitVec 32))(declare-fun |main::y@13| () (_ BitVec 32))(assert (and (= (bvadd (_ bv1 32) |main::i@18|) |main::i@19|) (and (and (and (bvslt |main::i@18| |main::edgecount@2|) (= |main::x@13| (select *int@9 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::i@18| (_ bv2 32)))))) (= |main::y@13| (select *int@9 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::i@18| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@13| (_ bv2 32)))) (select *int@9 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::i@18| (_ bv2 32))))) (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@13| (_ bv2 32)))))))))";
static char* formula7 = "(declare-fun |main::i@6| () (_ BitVec 32))(declare-fun *int@4 () (Array (_ BitVec 32) (_ BitVec 32)))(assert (and (or (and (and (bvslt |main::i@5| |main::nodecount@2|) (not (= |main::source@2| |main::i@5|))) (= *int@4 (store *int@3 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::i@5| (_ bv2 32))) INFINITY@2))) (and (and (bvslt |main::i@5| |main::nodecount@2|) (= |main::source@2| |main::i@5|)) (= *int@4 (store *int@3 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::i@5| (_ bv2 32))) (_ bv0 32))))) (= |main::i@6| (bvadd (_ bv1 32) |main::i@5|))))";
static char* formula8 = "(declare-fun |main::i@17| () (_ BitVec 32))(declare-fun |main::x@12| () (_ BitVec 32))(declare-fun |main::y@12| () (_ BitVec 32))(assert (and (= (bvadd (_ bv1 32) |main::i@17|) |main::i@18|) (and (and (and (bvslt |main::i@17| |main::edgecount@2|) (= |main::x@12| (select *int@9 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::i@17| (_ bv2 32)))))) (= |main::y@12| (select *int@9 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::i@17| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@12| (_ bv2 32)))) (select *int@9 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::i@17| (_ bv2 32))))) (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@12| (_ bv2 32)))))))))";
static char* formula9 = "(declare-fun |main::i@7| () (_ BitVec 32))(declare-fun *int@5 () (Array (_ BitVec 32) (_ BitVec 32)))(assert (and (or (and (and (bvslt |main::i@6| |main::nodecount@2|) (not (= |main::source@2| |main::i@6|))) (= *int@5 (store *int@4 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::i@6| (_ bv2 32))) INFINITY@2))) (and (and (bvslt |main::i@6| |main::nodecount@2|) (= |main::source@2| |main::i@6|)) (= *int@5 (store *int@4 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::i@6| (_ bv2 32))) (_ bv0 32))))) (= |main::i@7| (bvadd (_ bv1 32) |main::i@6|))))";
static char* formula10 = "(declare-fun |main::i@16| () (_ BitVec 32))(declare-fun |main::x@11| () (_ BitVec 32))(declare-fun |main::y@11| () (_ BitVec 32))(assert (and (= (bvadd (_ bv1 32) |main::i@16|) |main::i@17|) (and (and (and (bvslt |main::i@16| |main::edgecount@2|) (= |main::x@11| (select *int@9 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::i@16| (_ bv2 32)))))) (= |main::y@11| (select *int@9 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::i@16| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@11| (_ bv2 32)))) (select *int@9 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::i@16| (_ bv2 32))))) (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@11| (_ bv2 32)))))))))";
static char* formula11 = "(declare-fun |main::i@8| () (_ BitVec 32))(declare-fun *int@6 () (Array (_ BitVec 32) (_ BitVec 32)))(assert (and (= (bvadd (_ bv1 32) |main::i@7|) |main::i@8|) (or (and (and (bvslt |main::i@7| |main::nodecount@2|) (not (= |main::source@2| |main::i@7|))) (= *int@6 (store *int@5 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::i@7| (_ bv2 32))) INFINITY@2))) (and (and (bvslt |main::i@7| |main::nodecount@2|) (= |main::source@2| |main::i@7|)) (= *int@6 (store *int@5 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::i@7| (_ bv2 32))) (_ bv0 32)))))))";
static char* formula12 = "(declare-fun |main::i@15| () (_ BitVec 32))(declare-fun |main::x@10| () (_ BitVec 32))(declare-fun |main::y@10| () (_ BitVec 32))(assert (and (= (bvadd (_ bv1 32) |main::i@15|) |main::i@16|) (and (and (and (bvslt |main::i@15| |main::edgecount@2|) (= |main::x@10| (select *int@9 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::i@15| (_ bv2 32)))))) (= |main::y@10| (select *int@9 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::i@15| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@10| (_ bv2 32)))) (select *int@9 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::i@15| (_ bv2 32))))) (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@10| (_ bv2 32)))))))))";
static char* formula13 = "(declare-fun |main::i@9| () (_ BitVec 32))(assert (and (not (bvslt |main::i@8| |main::nodecount@2|)) (= |main::i@9| (_ bv0 32))))";
static char* formula14 = "(declare-fun |main::i@14| () (_ BitVec 32))(declare-fun |main::x@9| () (_ BitVec 32))(declare-fun |main::y@9| () (_ BitVec 32))(assert (and (= (bvadd (_ bv1 32) |main::i@14|) |main::i@15|) (and (and (and (bvslt |main::i@14| |main::edgecount@2|) (= |main::x@9| (select *int@9 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::i@14| (_ bv2 32)))))) (= |main::y@9| (select *int@9 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::i@14| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@9| (_ bv2 32)))) (select *int@9 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::i@14| (_ bv2 32))))) (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@9| (_ bv2 32)))))))))";
static char* formula15 = "(declare-fun |main::j@3| () (_ BitVec 32))(assert (and (bvslt |main::i@9| |main::nodecount@2|) (= |main::j@3| (_ bv0 32))))";
static char* formula16 = "(declare-fun |main::i@13| () (_ BitVec 32))(declare-fun |main::x@8| () (_ BitVec 32))(declare-fun |main::y@8| () (_ BitVec 32))(assert (and (= (bvadd (_ bv1 32) |main::i@13|) |main::i@14|) (and (and (and (bvslt |main::i@13| |main::edgecount@2|) (= |main::x@8| (select *int@9 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::i@13| (_ bv2 32)))))) (= |main::y@8| (select *int@9 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::i@13| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@8| (_ bv2 32)))) (select *int@9 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::i@13| (_ bv2 32))))) (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@8| (_ bv2 32)))))))))";
static char* formula17 = "(declare-fun |main::x@3| () (_ BitVec 32))(declare-fun |main::y@3| () (_ BitVec 32))(declare-fun *int@7 () (Array (_ BitVec 32) (_ BitVec 32)))(declare-fun |main::j@4| () (_ BitVec 32))(assert (and (or (and (and (and (and (bvslt |main::j@3| |main::edgecount@2|) (= |main::x@3| (select *int@6 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::j@3| (_ bv2 32)))))) (= |main::y@3| (select *int@6 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::j@3| (_ bv2 32)))))) (bvslt (bvadd (select *int@6 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@3| (_ bv2 32)))) (select *int@6 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::j@3| (_ bv2 32))))) (select *int@6 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@3| (_ bv2 32)))))) (= *int@7 (store *int@6 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@3| (_ bv2 32))) (bvadd (select *int@6 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@3| (_ bv2 32)))) (select *int@6 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::j@3| (_ bv2 32)))))))) (and (and (and (and (bvslt |main::j@3| |main::edgecount@2|) (= |main::x@3| (select *int@6 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::j@3| (_ bv2 32)))))) (= |main::y@3| (select *int@6 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::j@3| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@6 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@3| (_ bv2 32)))) (select *int@6 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::j@3| (_ bv2 32))))) (select *int@6 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@3| (_ bv2 32))))))) (= *int@6 *int@7))) (= (bvadd (_ bv1 32) |main::j@3|) |main::j@4|)))";
static char* formula18 = "(declare-fun |main::i@12| () (_ BitVec 32))(declare-fun |main::x@7| () (_ BitVec 32))(declare-fun |main::y@7| () (_ BitVec 32))(assert (and (= (bvadd (_ bv1 32) |main::i@12|) |main::i@13|) (and (and (and (bvslt |main::i@12| |main::edgecount@2|) (= |main::x@7| (select *int@9 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::i@12| (_ bv2 32)))))) (= |main::y@7| (select *int@9 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::i@12| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@7| (_ bv2 32)))) (select *int@9 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::i@12| (_ bv2 32))))) (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@7| (_ bv2 32)))))))))";
static char* formula19 = "(declare-fun |main::x@4| () (_ BitVec 32))(declare-fun |main::y@4| () (_ BitVec 32))(declare-fun *int@8 () (Array (_ BitVec 32) (_ BitVec 32)))(declare-fun |main::j@5| () (_ BitVec 32))(assert (and (or (and (and (and (and (bvslt |main::j@4| |main::edgecount@2|) (= |main::x@4| (select *int@7 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::j@4| (_ bv2 32)))))) (= |main::y@4| (select *int@7 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::j@4| (_ bv2 32)))))) (bvslt (bvadd (select *int@7 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@4| (_ bv2 32)))) (select *int@7 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::j@4| (_ bv2 32))))) (select *int@7 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@4| (_ bv2 32)))))) (= *int@8 (store *int@7 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@4| (_ bv2 32))) (bvadd (select *int@7 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@4| (_ bv2 32)))) (select *int@7 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::j@4| (_ bv2 32)))))))) (and (and (and (and (bvslt |main::j@4| |main::edgecount@2|) (= |main::x@4| (select *int@7 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::j@4| (_ bv2 32)))))) (= |main::y@4| (select *int@7 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::j@4| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@7 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@4| (_ bv2 32)))) (select *int@7 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::j@4| (_ bv2 32))))) (select *int@7 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@4| (_ bv2 32))))))) (= *int@7 *int@8))) (= (bvadd (_ bv1 32) |main::j@4|) |main::j@5|)))";
static char* formula20 = "(declare-fun |main::i@11| () (_ BitVec 32))(declare-fun |main::x@6| () (_ BitVec 32))(declare-fun |main::y@6| () (_ BitVec 32))(assert (and (= (bvadd (_ bv1 32) |main::i@11|) |main::i@12|) (and (and (and (bvslt |main::i@11| |main::edgecount@2|) (= |main::x@6| (select *int@9 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::i@11| (_ bv2 32)))))) (= |main::y@6| (select *int@9 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::i@11| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@6| (_ bv2 32)))) (select *int@9 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::i@11| (_ bv2 32))))) (select *int@9 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@6| (_ bv2 32)))))))))";
static char* formula21 = "(declare-fun |main::x@5| () (_ BitVec 32))(declare-fun |main::y@5| () (_ BitVec 32))(declare-fun |main::j@6| () (_ BitVec 32))(assert (and (or (and (and (and (and (bvslt |main::j@5| |main::edgecount@2|) (= |main::x@5| (select *int@8 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::j@5| (_ bv2 32)))))) (= |main::y@5| (select *int@8 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::j@5| (_ bv2 32)))))) (bvslt (bvadd (select *int@8 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@5| (_ bv2 32)))) (select *int@8 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::j@5| (_ bv2 32))))) (select *int@8 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@5| (_ bv2 32)))))) (= *int@9 (store *int@8 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@5| (_ bv2 32))) (bvadd (select *int@8 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@5| (_ bv2 32)))) (select *int@8 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::j@5| (_ bv2 32)))))))) (and (and (and (and (bvslt |main::j@5| |main::edgecount@2|) (= |main::x@5| (select *int@8 (bvadd |__ADDRESS_OF_main::Dest@| (bvshl |main::j@5| (_ bv2 32)))))) (= |main::y@5| (select *int@8 (bvadd |__ADDRESS_OF_main::Source@| (bvshl |main::j@5| (_ bv2 32)))))) (not (bvslt (bvadd (select *int@8 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::y@5| (_ bv2 32)))) (select *int@8 (bvadd |__ADDRESS_OF_main::Weight@| (bvshl |main::j@5| (_ bv2 32))))) (select *int@8 (bvadd |__ADDRESS_OF_main::distance@| (bvshl |main::x@5| (_ bv2 32))))))) (= *int@8 *int@9))) (= (bvadd (_ bv1 32) |main::j@5|) |main::j@6|)))";
static char* formula22 = "(declare-fun |main::i@10| () (_ BitVec 32))(assert (and (not (bvslt |main::i@10| |main::nodecount@2|)) (= |main::i@11| (_ bv0 32))))";
static char* formula23 = "(assert (and (= (bvadd (_ bv1 32) |main::i@9|) |main::i@10|) (not (bvslt |main::j@6| |main::edgecount@2|))))";

static const char* configString = "verbosity=0\n"
                                  "proof_generation=true\n"
                                  "interpolation=true\n"
                                  "model_generation=true\n"
                                  "bool_model_generation=false\n"
                                  "unsat_core_generation=0\n"
                                  "random_seed=42\n"
                                  "debug.dump_theory_lemmas=false\n"
                                  "debug.solver_enabled=true\n"
                                  "printer.bv_number_format=0\n"
                                  "printer.fp_number_format=1\n"
                                  "printer.defines_prefix=\n"
                                  "printer.model_as_formula=false\n"
                                  "preprocessor.toplevel_propagation=false\n"
                                  "preprocessor.toplevel_propagation_limit=0\n"
                                  "preprocessor.simplification=23\n"
                                  "preprocessor.ite_minimization=false\n"
                                  "preprocessor.ite_minimization_call_limit=150000\n"
                                  "preprocessor.interpolation_ite_elimination=false\n"
                                  "preprocessor.partial_nnf_conversion=false\n"
                                  "preprocessor.full_cnf_conversion=false\n"
                                  "dpll.restart_strategy=0\n"
                                  "dpll.restart_initial=200\n"
                                  "dpll.restart_geometric_factor=1.5\n"
                                  "dpll.store_tlemmas=false\n"
                                  "dpll.branching_random_frequency=0.001\n"
                                  "dpll.branching_initial_phase=0\n"
                                  "dpll.branching_cache_phase=2\n"
                                  "dpll.branching_random_invalidate_phase_cache=false\n"
                                  "dpll.branching_random_ignore_polarity=true\n"
                                  "dpll.ghost_filtering=true\n"
                                  "dpll.minimize_model=false\n"
                                  "dpll.allsat_minimize_model=false\n"
                                  "dpll.allsat_allow_duplicates=false\n"
                                  "dpll.pop_btpoint_reset_var_order=true\n"
                                  "dpll.glucose_var_activity=false\n"
                                  "dpll.glucose_learnt_minimization=false\n"
                                  "dpll.interpolation_mode=0\n"
                                  "dpll.proof_simplification=false\n"
                                  "dpll.preprocessor.mode=0\n"
                                  "dpll.preprocessor.clause_size_limit=20\n"
                                  "dpll.preprocessor.subsumption_size_limit=1000\n"
                                  "dpll.preprocessor.elimination_grow_limit=0\n"
                                  "dpll.preprocessor.elimination_phase=1\n"
                                  "dpll.preprocessor.elimination_recent_vars_only=false\n"
                                  "dpll.preprocessor.try_reelimination=true\n"
                                  "theory.eq_propagation=true\n"
                                  "theory.interface_eq_policy=2\n"
                                  "theory.pairwise_interface_eq=true\n"
                                  "theory.interface_eq_batch_size=100\n"
                                  "theory.pure_literal_filtering=false\n"
                                  "theory.euf.enabled=true\n"
                                  "theory.euf.dyn_ack=0\n"
                                  "theory.euf.dyn_ack_threshold=1\n"
                                  "theory.euf.dyn_ack_limit=1000\n"
                                  "theory.la.enabled=true\n"
                                  "theory.la.split_rat_eq=false\n"
                                  "theory.la.delay_alien=false\n"
                                  "theory.la.pivoting_greedy_threshold=0\n"
                                  "theory.la.lazy_expl_threshold=10\n"
                                  "theory.la.interpolation_laz_use_floor=true\n"
                                  "theory.la.pure_equality_filtering=true\n"
                                  "theory.la.detect_euf_fragment=false\n"
                                  "theory.la.deduction_enabled=true\n"
                                  "theory.la.laz_equality_elimination=true\n"
                                  "theory.la.laz_internal_branch_and_bound=true\n"
                                  "theory.la.laz_internal_branch_and_bound_limit=1\n"
                                  "theory.la.laz_cuts_from_proofs_mode=3\n"
                                  "theory.la.laz_enabled=true\n"
                                  "theory.la.laz_unit_cube_test=true\n"
                                  "theory.la.interpolation_mode=0\n"
                                  "theory.bv.enabled=true\n"
                                  "theory.bv.div_by_zero_mode=0\n"
                                  "theory.bv.delay_propagated_eqs=true\n"
                                  "theory.bv.eager=false\n"
                                  "theory.bv.bit_blast_mode=1\n"
                                  "theory.bv.interpolation_mode=0\n"
                                  "theory.bv.proof_simplification=false\n"
                                  "theory.bv.lazydpll.restart_strategy=0\n"
                                  "theory.bv.lazydpll.restart_initial=200\n"
                                  "theory.bv.lazydpll.restart_geometric_factor=1.5\n"
                                  "theory.bv.lazydpll.branching_random_frequency=0\n"
                                  "theory.bv.lazydpll.branching_initial_phase=0\n"
                                  "theory.bv.lazydpll.branching_cache_phase=2\n"
                                  "theory.bv.lazydpll.branching_random_invalidate_phase_cache=false\n"
                                  "theory.bv.lazydpll.branching_random_ignore_polarity=true\n"
                                  "theory.bv.lazydpll.ghost_filtering=false\n"
                                  "theory.bv.lazydpll.glucose_var_activity=false\n"
                                  "theory.bv.lazydpll.glucose_learnt_minimization=false\n"
                                  "theory.arr.enabled=true\n"
                                  "theory.arr.mode=0\n"
                                  "theory.arr.lazy_lemmas=false\n"
                                  "theory.arr.max_ext_lemmas=0\n"
                                  "theory.arr.enable_ext_polarity=true\n"
                                  "theory.arr.enable_ext_arg=true\n"
                                  "theory.arr.enable_witness=true\n"
                                  "theory.fp.enabled=true\n"
                                  "theory.fp.minmax_zero_mode=1\n"
                                  "theory.fp.mode=1\n"
                                  "theory.fp.bv_combination_enabled=true\n"
                                  "theory.fp.bit_blast_mode=2\n"
                                  "theory.fp.dpll.restart_strategy=3\n"
                                  "theory.fp.dpll.restart_initial=200\n"
                                  "theory.fp.dpll.restart_geometric_factor=1.5\n"
                                  "theory.fp.dpll.branching_random_frequency=0.01\n"
                                  "theory.fp.dpll.branching_initial_phase=0\n"
                                  "theory.fp.dpll.branching_cache_phase=1\n"
                                  "theory.fp.dpll.branching_random_invalidate_phase_cache=false\n"
                                  "theory.fp.dpll.branching_random_ignore_polarity=true\n"
                                  "theory.fp.dpll.ghost_filtering=false\n"
                                  "theory.fp.dpll.glucose_var_activity=true\n"
                                  "theory.fp.dpll.glucose_learnt_minimization=true\n"
                                  "theory.fp.acdcl_conflict_generalization=2\n"
                                  "theory.fp.interpolation_mode=0\n"
                                  "theory.fp.acdcl_single_propagation_limit=0\n"
                                  "theory.fp.acdcl_single_generalization_limit=0\n"
                                  "theory.fp.acdcl_generalization_fair=true\n"
                                  "theory.na.enabled=true\n"
                                  "theory.na.permanent_lemmas=true\n"
                                  "theory.na.eager_lemmas=false\n"
                                  "theory.na.enable_tangent_lemmas_frontier=true\n"
                                  "theory.na.tangent_lemmas_rat_approx=0\n"
                                  "theory.na.tangent_lemmas_limit=0\n"
                                  "theory.na.tangent_lemmas_enabled=true\n"
                                  "theory.na.sat_check_enabled=true\n"
                                  "theory.na.bound_lemmas_enabled=true\n"
                                  "theory.na.nta_enabled=true\n"
                                  "theory.na.nta_rat_approx=3\n"
                                  "theory.na.nta_rat_approx_limit=10\n"
                                  "theory.na.nta_sat_mode=1\n"
                                  "theory.na.nta_eager=true";

// Taken directly from example on the mathsat webpage
static void print_model(msat_env env){
    msat_model_iterator iter = msat_create_model_iterator(env);
    assert(!MSAT_ERROR_MODEL_ITERATOR(iter));

    printf("Model:\n");
    while (msat_model_iterator_has_next(iter)) {
        msat_term t, v;
        char *s;
        msat_model_iterator_next(iter, &t, &v);
        s = msat_term_repr(t);
        assert(s);
        printf(" %s = ", s);
        msat_free(s);
        s = msat_term_repr(v);
        assert(s);
        printf("%s\n", s);
        msat_free(s);
    }
    msat_destroy_model_iterator(iter);
}

static void interpolationCrashExample(){
    msat_config cfg;
    msat_env env;
    msat_result status;
    msat_term formula;
    int res, group0, group1, group2, group3, group4, group5, group6, group7, group8, group9, group10, group11, group12, group13, group14, group15, group16, group17, group18, group19, group21, group22, group23;
    char *s;
    // All interpolation groups
    int interpolationGroups[] = {group0, group1, group2, group3, group4, group5, group6, group7, group8, group9, group10, group11, group12, group13, group14, group15, group16, group17, group18, group19, group21, group22, group23};
    // All formulas as Strings
    char* formulaArray[] = {formula0, formula1, formula2, formula3, formula4, formula5, formula6, formula7, formula8, formula9, formula10, formula11, formula12, formula13, formula14, formula15, formula16, formula17, formula18, formula19, formula20, formula21, formula22, formula23};
    //Array of Names of Arrays Bitvec32 Bitvec32
    char* bitvec32ArrayArray[] = {"*int@9", "*int@1", "*int@2", "*int@3", "*int@4", "*int@5", "*int@6", "*int@7", "*int@8"};
    char* bitvec32Array[] = {"|main::nodecount@2|", "|__ADDRESS_OF_main::distance@|", "|__VERIFIER_assert::cond@2|", "|main::i@21|", "INFINITY@2", "|main::edgecount@2|", "|main::source@2|", "|__ADDRESS_OF_main::Source@|", "|__ADDRESS_OF_main::Dest@|", "|__ADDRESS_OF_main::Weight@|", "|main::i@3|", "|main::i@20|", "|main::i@4|", "|main::i@19|", "|main::x@14|", "|main::y@14|", "|main::i@5|", "|main::i@18|", "|main::x@13|", "|main::y@13|", "|main::i@6|", "|main::i@17|", "|main::x@12|", "|main::y@12|", "|main::i@7|", "|main::i@16|", "|main::x@11|", "|main::y@11|", "|main::i@8|", "|main::i@15|", "|main::x@10|", "|main::y@10|", "|main::i@9|", "|main::i@14|", "|main::x@9|", "|main::y@9|", "|main::j@3|", "|main::i@13|", "|main::x@8|", "|main::y@8|", "|main::x@3|", "|main::y@3|", "|main::j@4|", "|main::i@12|", "|main::x@7|", "|main::y@7|", "|main::x@4|", "|main::y@4|", "|main::j@5|", "|main::i@11|", "|main::x@6|", "|main::y@6|", "|main::x@5|", "|main::y@5|", "|main::j@6|", "|main::i@10|"};

    printf("\nExample start\n");

    /* We parse the config used in our use-case */
    cfg = msat_parse_config(configString);
    assert(!MSAT_ERROR_CONFIG(cfg));

    env = msat_create_env(cfg);
    assert(!MSAT_ERROR_ENV(env));

    msat_type bv32_tp = msat_get_bv_type(env, 32);
    //Only this kind of array is used
    msat_type array_tp = msat_get_array_type(env, bv32_tp, bv32_tp);

    //Trust me its 56!
    for (int i = 0; i < 56; ++i) {
        msat_decl d = msat_declare_function(env, bitvec32Array[i], bv32_tp);
        assert(!MSAT_ERROR_DECL(d));
    }

    for (int i = 0; i < sizeof(bitvec32ArrayArray)/sizeof(bitvec32ArrayArray[0]); ++i) {
        msat_decl d = msat_declare_function(env, bitvec32ArrayArray[i], array_tp);
        assert(!MSAT_ERROR_DECL(d));
    }

    /* create formulas from smtlib2, then set interpolation group and assert the formula */
    for(int i = 0; i < 24; i++) {
      msat_push_backtrack_point(env);
      formula = msat_from_smtlib2(env, formulaArray[i]);
      assert(!MSAT_ERROR_TERM(formula));

      interpolationGroups[i] = msat_create_itp_group(env);
      assert(interpolationGroups[i] != -1);
      res = msat_set_itp_group(env, interpolationGroups[i]);
      assert(res == 0);

      res = msat_assert_formula(env, formula);
      assert(res == 0);

      {
        s = msat_term_repr(formula);
        assert(s);
        printf("\nAdded constraint number %d: \n%s\n\n", i, s);
        msat_free(s);
      }

      status = msat_solve(env);

      if (status == MSAT_UNSAT) {
        printf("Result: UNSAT\n");
      } else if (status == MSAT_SAT) {
        printf("Result: SAT.\n");
      } else {
        printf("Result: Unknown. That should not happen.\n");
      }
    }

    printf("\n");
    if (status == MSAT_UNSAT) {
      printf("Last Result: UNSAT\n");
      int groups_of_1[1];
      msat_term interpolant;
      char *t;
      groups_of_1[0] = group0;
      interpolant = msat_get_interpolant(env, groups_of_1, 1);
      //assert(!MSAT_ERROR_TERM(interpolant));
      t = msat_term_repr(interpolant);
      assert(t);
      printf("\nOK, the interpolant is: %s\n", t);
      msat_free(t);
    } else if (status == MSAT_SAT) {
      printf("Last Result: SAT. That should not happen.\n");
    } else {
      printf("Last Result: Unknown. That should not happen.\n");
    }

    msat_destroy_env(env);
    msat_destroy_config(cfg);

    printf("\nEnd of example\n");
}

int main(){
    printf("This example illustrates a SegFault when interpolation is used\n");

    interpolationCrashExample();

    return 0;
}
baierd commented 4 years ago

Status: Reported to Alberto

baierd commented 4 years ago

Alberto answered that this is most likely a result of mixing theories (Bv/Array) and we have to live with it.

Note: We are checking for the return values in the JNI-Wrapper via a macro, so no issue there.

kfriedberger commented 4 years ago

It seems as if we mixed up two different issues here:

Please sort out which part of this conversation belongs to which issue. Maybe we should close this interleaved issue and open another issue for the SegFault.

baierd commented 4 years ago

This is of course for the interpolation issue and not the SigSev.

The interpolation issue just emerged when trying to find the SigSev. The problem is more that the next step to find the SigSev would be tracking every single command/input the CPAchecker uses in JavaSMT and recreate it with the hopes of causing the SigSev. You mentioned that this might be overkill for this issue but now i realize that you might have thought of the interpolation issue and not the SigSev, do you want me to track down the SigSev further?

kfriedberger commented 4 years ago

As the SegFault does not appear that often, it has a minor priority.

Instead of manually tracking down every call, one could dump all native calls as part of the JNI wrapper. One could add some logging into the C-code and dump all queries in some form of direct C-code. An execution of CPAchecker would then produce a full interaction log on native level.

Dummy example:

int foo(int x) {
  int ret = call_foo(x);
  log("int " + id(ret) + " = call_foo(" + id(x) + ");")
  return ret;
}

where id returns a unique string identifier for every pointer and variable, and perhaps the plain in for real integers. As our JNI wrapper already uses macros, there might only be a few places, where such code might be required. The difficulty is that our macros are written in a very generic way, and String handling in C is hard.

baierd commented 4 years ago

I'm going to take a look at it. A naive test for feasibility shouldn't be too hard.