| | | | |
| Offset 44619, 15 lines modified | Offset 44619, 15 lines modified |
| 44619 | sat::rnd_decisiosat::propagationsat::clauses_litsat::learnts_litsat::max_literalsat::tot_literal./src/prop/minisat/simp/SimpSolvset-user-attribudeclare-primed-vexpand-definitioget-instantiatioreset-assertionscheck-sat-assumiget-unsat-assumpblock-model-valudeclare-datatypeassertions:post-produce-assertioproduce-assignmeUnrecognized·informational·or·option·key·or·settsmt::SmtEngine::definitionExpansnumConstantPropscnfConversionTimnumAssertionsPrenumAssertionsPoslfscCheckProofTicheckUnsatCoreTiprocessAssertionsimplifiedToFalsresourceUnitsUsez::approx::brancz::approx::gaussianElimConstructz::approx::avera | 44619 | sat::rnd_decisiosat::propagationsat::clauses_litsat::learnts_litsat::max_literalsat::tot_literal./src/prop/minisat/simp/SimpSolvset-user-attribudeclare-primed-vexpand-definitioget-instantiatioreset-assertionscheck-sat-assumiget-unsat-assumpblock-model-valudeclare-datatypeassertions:post-produce-assertioproduce-assignmeUnrecognized·informational·or·option·key·or·settsmt::SmtEngine::definitionExpansnumConstantPropscnfConversionTimnumAssertionsPrenumAssertionsPoslfscCheckProofTicheckUnsatCoreTiprocessAssertionsimplifiedToFalsresourceUnitsUsez::approx::brancz::approx::gaussianElimConstructz::approx::avera |
| 44620 | theory::arith::iteMinMaxApplicatteConstantApplictheory::arith::attempt::searchTittempt::queueTimttempt::conflicttheory::arith::congruence::watchedVariableIsZeroedVariableIsNotZongruence::equalongruence::propaongruence::confltheory::arith::ArithCongruenceMad::unatePropagattheory::arith::dio::conflictCallio::conflictTimeis·an·integer·variable·created·by·the·dio·solverual::UpdateConflual::findConflicual::simplexConfual::recentViolatheory::arith::pqueue::enqueuesCqueue::enqueuesDqueue::enqueuesVollectionDuplicaarOrderModeDuplitheory::arith::FC::initialProcesC::UpdateConflicC::selectUpdateFtheory::arith::utheory::arith::weakening::attempeakening::succestheory::arith::f | 44620 | theory::arith::iteMinMaxApplicatteConstantApplictheory::arith::attempt::searchTittempt::queueTimttempt::conflicttheory::arith::congruence::watchedVariableIsZeroedVariableIsNotZongruence::equalongruence::propaongruence::confltheory::arith::ArithCongruenceMad::unatePropagattheory::arith::dio::conflictCallio::conflictTimeis·an·integer·variable·created·by·the·dio·solverual::UpdateConflual::findConflicual::simplexConfual::recentViolatheory::arith::pqueue::enqueuesCqueue::enqueuesDqueue::enqueuesVollectionDuplicaarOrderModeDuplitheory::arith::FC::initialProcesC::UpdateConflicC::selectUpdateFtheory::arith::utheory::arith::weakening::attempeakening::succestheory::arith::f |
| 44621 | phase·shifted·trtheory::arith::SOI::initialProceOI::UpdateConfliOI::ConfMin::numOI::ConstructionOI::Conflict::Mian·extensional·lemma·index·variable·from·the·theabstraction·function·for·bv·theotheory::bv::algebraic::NumCallsTbraic::NumSimplibraic::NumUnknowbraic::SolveTimebraic::UseHeuristheory::bv::BitblastSolver::NumClastSolver::NumTtheory::bv::lazytheory::bv::CoreSolver::NumCallsSolver::SlicerEntheory::bv::inequality::NumCallsuality::SolveTimtheory::bv::slicer::NumRepresenter::AverageFindDer::NumEqualitietheory::bv::AvgBtheory::bv::NumSolveSubstitutiontheory::bv::solvtheory::bv::NumFtandardCheckCalltheory::bv::weightComputationTimtheory::bv::NumMeated·by·the·theory·of·bitvectorEagerProofGeneraA·boolean·variable·asserted·to·be·true·to·force· | 44621 | phase·shifted·trtheory::arith::SOI::initialProceOI::UpdateConfliOI::ConfMin::numOI::ConstructionOI::Conflict::Mian·extensional·lemma·index·variable·from·the·theabstraction·function·for·bv·theotheory::bv::algebraic::NumCallsTbraic::NumSimplibraic::NumUnknowbraic::SolveTimebraic::UseHeuristheory::bv::BitblastSolver::NumClastSolver::NumTtheory::bv::lazytheory::bv::CoreSolver::NumCallsSolver::SlicerEntheory::bv::inequality::NumCallsuality::SolveTimtheory::bv::slicer::NumRepresenter::AverageFindDer::NumEqualitietheory::bv::AvgBtheory::bv::NumSolveSubstitutiontheory::bv::solvtheory::bv::NumFtandardCheckCalltheory::bv::weightComputationTimtheory::bv::NumMeated·by·the·theory·of·bitvectorEagerProofGeneraA·boolean·variable·asserted·to·be·true·to·force· |
| 44622 | variable·to·represent·disjoint·efree·infinity·for·virtual·term·sinfinity·for·virtual·term·substifree·delta·for·virtual·term·subsdelta·for·virtual·term·substitutConjectureGenerawas·created·by·conjecture·ground·term·enumeratorinternal·op·for·dynamic_rewritersygus-rr-synth-iskolem·created·for·full-model·chop·for·full-modeop·created·durinInstStrategyEnumInstantiate::Instantiations_TotaInstantiate::Duplicate_Inst_Entalicate_Inst_ModeQuantConflictFind::Entailment_ChEPR·base·constancreated·during·sg·pre-skolemizatCannot·get·synth·function:·reconstruction·to·syncegis_unif_num_e | 44622 | variable·to·represent·disjoint·efree·infinity·for·virtual·term·sinfinity·for·virtual·term·substifree·delta·for·virtual·term·subsdelta·for·virtual·term·substitutConjectureGenerawas·created·by·conjecture·ground·term·enumeratorinternal·op·for·dynamic_rewritersygus-rr-synth-iskolem·created·for·full-model·chop·for·full-modeop·created·durinInstStrategyEnumInstantiate::Instantiations_TotaInstantiate::Duplicate_Inst_Entalicate_Inst_ModeQuantConflictFind::Entailment_ChEPR·base·constancreated·during·sg·pre-skolemizatCannot·get·synth·function:·reconstruction·to·syncegis_unif_num_e |
| 44623 | miniscope-quant-SynthEngine::cegqi_lemmas_refineSynthConjecture::filtered_soluti:candidate_rewriSygusEnumerator::enumTermsRewrit:enumTermsEvalEx | 44623 | miniscope-quant-SynthEngine::cegqi_lemmas_refineSynthConjecture::filtered_soluti:candidate_rewriSygusEnumerator::enumTermsRewrit:enumTermsEvalEx |
| 44624 | head·of·unif·evaqe·for·non-ground·single·invocatqe·for·function·in·non-ground·sifor·sygus·invaritemplate·inferenis·a·termDb·frespredicate·to·force·higher-order·TheoryQuantifiercardinality·bound·element·for·setheory::sets::eetheory::shared_tSharedTermsDatabtheory::strings::cdSimplificatio:regexpUnfolding:conflictsEqEngi:conflictsEagerP:lemmasEagerPrep:lemmasRegisterTstring·purify·sk | 44624 | head·of·unif·evaqe·for·non-ground·single·invocatqe·for·function·in·non-ground·sifor·sygus·invaritemplate·inferenis·a·termDb·frespredicate·to·force·higher-order·TheoryQuantifiercardinality·bound·element·for·setheory::sets::eetheory::shared_tSharedTermsDatabtheory::strings::cdSimplificatio:regexpUnfolding:conflictsEqEngi:conflictsEagerP:lemmasEagerPrep:lemmasRegisterTstring·purify·sk |
| 44625 | theory::datatypetheory::quantifiuf_combined_cardenumeration·to·meet·negative·car | 44625 | theory::datatypetheory::quantifiuf_combined_cardenumeration·to·meet·negative·car |
| 44626 | or·extensionalit2020-09-17·04:29this·expression·contains·an·element·of·unknown·type·(such·as·an·abstract·value);·its·type·cannot·be·computed·until·it·is·substitProofCheckerStatistics::ruleChecistics::totalRulPRefProofGeneratTConvProofGenerais·an·unresolved·selector·type·pis·a·shared·seleError·in·option·1844674407370955 | 44626 | or·extensionalit2020-09-18·06:29this·expression·contains·an·element·of·unknown·type·(such·as·an·abstract·value);·its·type·cannot·be·computed·until·it·is·substitProofCheckerStatistics::ruleChecistics::totalRulPRefProofGeneratTConvProofGenerais·an·unresolved·selector·type·pis·a·shared·seleError·in·option·1844674407370955 |
| 44627 | resource::Bitblaresource::BvEageresource::BvPropresource::BvSatCresource::CnfSteresource::Decisiresource::LemmaSresource::ParseSresource::Preproresource::Quantiresource::Restarresource::Rewritresource::SatConresource::Theory | 44627 | resource::Bitblaresource::BvEageresource::BvPropresource::BvSatCresource::CnfSteresource::Decisiresource::LemmaSresource::ParseSresource::Preproresource::Quantiresource::Restarresource::Rewritresource::SatConresource::Theory |
| 44628 | is·a·skolem·variable·imported·from·another·ExprM | 44628 | is·a·skolem·variable·imported·from·another·ExprM |
| 44629 | approx-branch-dearith-no-partialarith-prop-clausarith-rewrite-eqcollect-pivot-sterror-selection-heuristic-pivotsmaxCutsInContextnl-ext-tf-taylorpp-assert-max-suprop-row-length=replay-early-cloreplay-failure-preplay-num-err-preplay-reject-cureplay-soi-major-threshold-pen=Nreplay-soi-minorsimplex-check-pestandard-effort-variable-order-parrays-eager-indarrays-lazy-rintarrays-optimize-arrays-reduce-sharrays-weak-equistats-every-querstats-hide-zerosbv-algebraic-budbv-eager-explanabv-eq-slicer=MODbv-extract-arithbv-inequality-sobv-lazy-reduce-ebv-lazy-rewrite-bv-optimize-sat-bv-print-consts-as-indexed-symbobv-proof-format=dt-infer-as-lemmdt-rewrite-errorsygus-sym-break-decision-random-decision-threshodecision-use-weidecision-weight-print-expr-typesinteractive-promtear-down-incremfilesystem-accesglobal-declaratiflatten-ho-chaininst-format=MODEmodel-format=MODaggressive-core-allow-empty-depefewer-preprocesslfsc-letificatiominisat-dump-dimminisat-eliminatrandom-frequencyrefine-conflictsrestart-int-baserestart-int-inc=ag-miniscope-quacegis-sample=MODcegqi-bv-concat-cegqi-bv-ineq=MOcegqi-bv-interlecegqi-bv-rm-extrcegqi-bv-solve-ncegqi-multi-instcegqi-prereg-inscegqi-repeat-litcegqi-round-up-lcegqi-use-inf-incegqi-use-inf-recond-var-split-acond-var-split-qconjecture-filteconjecture-gen-gconjecture-gen-mconjecture-gen-pconjecture-gen-uconjecture-no-fidt-var-exp-quantelim-ext-arith-qext-rewrite-quanfinite-model-finfull-saturate-quho-elim-store-axho-matching-var-ho-merge-term-dbincrement-triggeinst-max-level=Ninst-no-model-trinst-when-phase=inst-when-strictinst-when-tc-firite-dtt-split-quite-lift-quant=Mliteral-matchinglte-restrict-insmacros-quant-modmbqi-one-inst-pemulti-trigger-camulti-trigger-prpartial-triggerspre-skolem-quantprenex-quant-useprenex-quant=MODpure-th-triggerspurify-dt-triggeqcf-all-conflictqcf-eager-check-qcf-nested-conflquant-anti-skolequant-cf-when=MOquant-dsplit-modquant-rep-mode=Mregister-quant-brelational-triggsygus-active-gensygus-add-const-sygus-arg-relevasygus-auto-unfolsygus-bool-ite-rsygus-core-connesygus-crepair-absygus-eval-unfolsygus-expr-miner-check-use-exporsygus-grammar-cosygus-grammar-nosygus-inv-templ-sygus-inv-templ=sygus-pbe-multi-sygus-qe-preprocsygus-query-gen-sygus-rec-fun-evsygus-repair-consygus-rr-synth-asygus-rr-synth-csygus-rr-synth-fsygus-rr-synth-rsygus-rr-verify-sygus-sample-fp-sygus-sample-grasygus-si-partialsygus-si-rcons-lsygus-si-rcons=Msygus-si-reconstsygus-templ-embesygus-unif-cond-independent-no-rsygus-unif-pi=MOsygus-unif-shuffsygus-verify-subterm-db-mode=MODtrack-inst-lemmatrigger-active-strigger-sel=MODEvar-ineq-elim-qusep-pre-skolem-esets-infer-as-lesets-proxy-lemmablock-models=MODbv-eager-assert-check-unsat-coredebug-check-modediagnostic-outpudump-instantiatidump-unsat-coresext-rew-prep-aggforce-no-limit-cinteractive-modemodel-cores=MODEmodel-witness-vaon-repeat-ite-siproduce-unsat-asproduce-unsat-coreproducible-ressat-conflict-stesimplification-msygus-print-calltheory-check-stere-inter-mode=MOstrings-guess-mostrings-infer-asstrings-infer-systrings-len-normstrings-min-prefstrings-print-asstrings-process-strings-rexplainassign-function-uf-symmetry-breauf-ss-abort-carduf-ss-totality-luf-ss-totality-sN4CVC47context10ContextObjE | 44629 | approx-branch-dearith-no-partialarith-prop-clausarith-rewrite-eqcollect-pivot-sterror-selection-heuristic-pivotsmaxCutsInContextnl-ext-tf-taylorpp-assert-max-suprop-row-length=replay-early-cloreplay-failure-preplay-num-err-preplay-reject-cureplay-soi-major-threshold-pen=Nreplay-soi-minorsimplex-check-pestandard-effort-variable-order-parrays-eager-indarrays-lazy-rintarrays-optimize-arrays-reduce-sharrays-weak-equistats-every-querstats-hide-zerosbv-algebraic-budbv-eager-explanabv-eq-slicer=MODbv-extract-arithbv-inequality-sobv-lazy-reduce-ebv-lazy-rewrite-bv-optimize-sat-bv-print-consts-as-indexed-symbobv-proof-format=dt-infer-as-lemmdt-rewrite-errorsygus-sym-break-decision-random-decision-threshodecision-use-weidecision-weight-print-expr-typesinteractive-promtear-down-incremfilesystem-accesglobal-declaratiflatten-ho-chaininst-format=MODEmodel-format=MODaggressive-core-allow-empty-depefewer-preprocesslfsc-letificatiominisat-dump-dimminisat-eliminatrandom-frequencyrefine-conflictsrestart-int-baserestart-int-inc=ag-miniscope-quacegis-sample=MODcegqi-bv-concat-cegqi-bv-ineq=MOcegqi-bv-interlecegqi-bv-rm-extrcegqi-bv-solve-ncegqi-multi-instcegqi-prereg-inscegqi-repeat-litcegqi-round-up-lcegqi-use-inf-incegqi-use-inf-recond-var-split-acond-var-split-qconjecture-filteconjecture-gen-gconjecture-gen-mconjecture-gen-pconjecture-gen-uconjecture-no-fidt-var-exp-quantelim-ext-arith-qext-rewrite-quanfinite-model-finfull-saturate-quho-elim-store-axho-matching-var-ho-merge-term-dbincrement-triggeinst-max-level=Ninst-no-model-trinst-when-phase=inst-when-strictinst-when-tc-firite-dtt-split-quite-lift-quant=Mliteral-matchinglte-restrict-insmacros-quant-modmbqi-one-inst-pemulti-trigger-camulti-trigger-prpartial-triggerspre-skolem-quantprenex-quant-useprenex-quant=MODpure-th-triggerspurify-dt-triggeqcf-all-conflictqcf-eager-check-qcf-nested-conflquant-anti-skolequant-cf-when=MOquant-dsplit-modquant-rep-mode=Mregister-quant-brelational-triggsygus-active-gensygus-add-const-sygus-arg-relevasygus-auto-unfolsygus-bool-ite-rsygus-core-connesygus-crepair-absygus-eval-unfolsygus-expr-miner-check-use-exporsygus-grammar-cosygus-grammar-nosygus-inv-templ-sygus-inv-templ=sygus-pbe-multi-sygus-qe-preprocsygus-query-gen-sygus-rec-fun-evsygus-repair-consygus-rr-synth-asygus-rr-synth-csygus-rr-synth-fsygus-rr-synth-rsygus-rr-verify-sygus-sample-fp-sygus-sample-grasygus-si-partialsygus-si-rcons-lsygus-si-rcons=Msygus-si-reconstsygus-templ-embesygus-unif-cond-independent-no-rsygus-unif-pi=MOsygus-unif-shuffsygus-verify-subterm-db-mode=MODtrack-inst-lemmatrigger-active-strigger-sel=MODEvar-ineq-elim-qusep-pre-skolem-esets-infer-as-lesets-proxy-lemmablock-models=MODbv-eager-assert-check-unsat-coredebug-check-modediagnostic-outpudump-instantiatidump-unsat-coresext-rew-prep-aggforce-no-limit-cinteractive-modemodel-cores=MODEmodel-witness-vaon-repeat-ite-siproduce-unsat-asproduce-unsat-coreproducible-ressat-conflict-stesimplification-msygus-print-calltheory-check-stere-inter-mode=MOstrings-guess-mostrings-infer-asstrings-infer-systrings-len-normstrings-min-prefstrings-print-asstrings-process-strings-rexplainassign-function-uf-symmetry-breauf-ss-abort-carduf-ss-totality-luf-ss-totality-sN4CVC47context10ContextObjE |
| 44630 | N4CVC47context16ContextNotifyObjE | 44630 | N4CVC47context16ContextNotifyObjE |
| 44631 | N4CVC47context6CDListINS_12NodeTemplateILb1EEENS0_14DefaultCleanUpIS3_EESaIS3_EEE | 44631 | N4CVC47context6CDListINS_12NodeTemplateILb1EEENS0_14DefaultCleanUpIS3_EESaIS3_EEE |
| 44632 | N4CVC47context3CDOINS_4prop8SatValueEEE | 44632 | N4CVC47context3CDOINS_4prop8SatValueEEE |
| 44633 | N4CVC48decision16DecisionStrategyE | 44633 | N4CVC48decision16DecisionStrategyE |