SRI-CSL / yices2

71%

LAST BUILD ON BRANCH master

branch: SELECT

CHANGE BRANCH

x

• No branch selected
• 2.6.5
• 2.7.0
• 2.8.0_doc_updates
• 2019-08-19
• 2019-08-19-mcsat-bv
• 2020-02-18
• 2020-08-19
• 2021-02-19
• 393-api-could-yices_assert_blocking_clause-return-the-clause
• 486-assertion-failure-in-srcmcsatvaluec-could-be-a-duplicate-of-451
• L2O_calc_update
• L2O_submission_merge
• Mrmaxmeier-smtlib-model-syntax
• Yices-2.5.3
• Yices-2.5.4
• Yices-2.6.0
• Yices-2.6.1
• Yices-2.6.2
• ahmed-irfan-debian
• ahmed-irfan-patch-1
• api-model-function-values
• api-test-eager-fail
• array-tests
• bool-bump-factor
• bool-scaling-20
• bugfix/608
• bugfix/issue-366
• bugfix/issue-406
• bvlra
• case-eval2
• cdclt-plugin
• change_no_error
• ci-coveralls-nonblocking
• ci-make-test
• ci_fixes
• codex/fw-egraph-satellite
• context_delegates
• cp-commit-02b6501
• cross-compile
• darpa-2019-02-19
• definition_clauses
• feature/wide-model-projection
• ff-api-extension
• fix-417-smt2-string-escape
• fix-640-clash-of-kittens
• fix-api-test
• fix-array-model-print-smt2
• fix-bv64-interval-abstraction-ub
• fix-check-api-warning
• fix-compilation-warnings
• fix-interpolant-with-empty-model
• fix-iss-392
• fix-iss-414
• fix-iss-433
• fix-iss-626-mcsat-ceil
• fix-issue-432
• fix-issue-534
• fix-issue-615-interpolation-crash
• fix-issue-616-cnf-gc-mark-static
• fix-issue-657
• fix-logic-order
• fix-mcsat-nira-eq-preprocessing
• fix-mcsat-param-api
• fix-portfolio-solver
• fix-smt2-echo-error-behavior
• fix-some-printing
• fix-strerror-mingw
• fix-timeout-mingw
• fix-unit-tests
• fix/iss552-root-pair-metadata
• fix/issue-403-getvalue-segfault
• fix/issue-536-bool-plugin-eval
• fix/smt2-array-model-format
• fix/threadsafe-disable-mcsat-cdclt-checks
• fix_array_solver_hash
• fix_binary_search
• fix_crashes
• fix_return
• hint-real-decisions
• implicant-cube-enumeration
• improve-ci-cache
• incr-cadical
• iss165-regression-test
• iss396-test
• iss410-reenable-intfeas
• iss440-fix
• iss547
• iss74-regression-test
• issue-613-mcsat-curried-function-model
• issue-621-plan-a-diff-witness
• issue517
• kissat_delegate
• master
• mcsat-api-var-order
• mcsat-array-comb
• mcsat-array-distinct
• mcsat-array-finite
• mcsat-array-improved-call
• mcsat-array-learn
• mcsat-array-patch-1
• mcsat-array-simplify-var-bump
• mcsat-array-sort-heuristic
• mcsat-arrays-2
• mcsat-arrays-fix
• mcsat-arrays-fixes
• mcsat-assumptions
• mcsat-boolean-lemma-minimization
• mcsat-bv
• mcsat-bv-array-purify
• mcsat-bv-refactorbdds
• mcsat-bv-smtcomp-2019
• mcsat-cached-value-tier-fallback
• mcsat-check-model-with-hint
• mcsat-eval-2
• mcsat-filter-binary-clauses
• mcsat-glue-reduce
• mcsat-imp-clause-db
• mcsat-imp-reducedb
• mcsat-incremental
• mcsat-int-hint-2
• mcsat-interpolation
• mcsat-keep-binary-clauses
• mcsat-learn
• mcsat-lemma-limit-update
• mcsat-model-hint
• mcsat-model-hint-registration-queue-fix
• mcsat-new-reduce
• mcsat-nra
• mcsat-nra-intervals
• mcsat-part-restart
• mcsat-recache
• mcsat-reduce
• mcsat-relax-zero-lemmas
• mcsat-set-initial-var-order-api
• mcsat-supplement-cdclt
• mcsat-target
• mcsat-target-best
• mcsat-test-option-update
• mcsat-trail-update-extra-cache-elements
• mcsat-tuples-support
• mcsat-ufnra-model-fix
• mcsat-unsat-core
• mcsat-update-heuristic
• mcsat-update-reduce
• mcsat_uf_model_fix
• mingw-special
• model-clone-project-api
• mt-master
• new-bv
• nra-cached-must-decide
• nra-hints-patch
• nra-learn-hint-next-decision
• nra-to-na
• nsat-target
• patch-iss-418-prerelease
• qf-eq-bv-arith
• rand-cmd
• reduce-cdclt
• refs/heads/mcsat_uf_model_fix
• refs/tags/Yices-2.6.5
• reintroduce-interval-approx-nra
• rename-smt-status-enum
• rename-yices-status-enum
• rm-scratch-compilation
• simpler-unsat-cores
• simplify-mcsat-randomness-setting
• size_t
• small_fixes
• smt2-algebraic-model-format
• smt2-output
• smt2-set-option-timeout
• smtcomp-2017
• smtcomp2020
• smtcomp2021
• smtcomp2024
• smtcomp2025
• smtlib-model-syntax
• test-451
• test-initial-order
• test-var-order
• tmp_good
• type-macros-api
• types-macros-doc
• unique-fun-decision
• untagged-ccae5cc58023f61e3a62
• update-actions-checkout-4
• update-ci
• update-ci-check-api
• update-cov
• update-html-doc
• update-set-var-oder-api
• update-weq-term-rep
• update-win-ci-thread-safety
• v
• valgrind-regress
• weq-fix-todo
• wide-projection-stats
• win-ci
• win-ci-2
• y2sat-multicheck-fix
• yices.py
• yices2-mcsat-portfolio-py

Build # 30150074613

Build Type

push

github

Committed by web-flow

Commit Message

Fix ef-solve crash and spurious "model error" on UF-in-arithmetic quantifiers (#657) (#658)

ef-solve on a forall body with an uninterpreted-function application inside
arithmetic (e.g. (f x) in (< x C)) crashed, and on release builds aborted with
a bogus "FATAL ERROR: ... model error" bug report. Two independent causes:

- quant_pattern.c walked terms with term_child, which only supports composite
  terms. Arithmetic/bitvector polynomials, products, and projections (which
  term_num_children still counts) hit term_child's composite path and read a
  wrong descriptor -> ASan/debug crash, release UB. Add a shared
  term_ith_subterm() in term_explorer.c that reads those components off the
  descriptor, and use it in the three quant pattern walkers.

- ef_generalize3 built a full model via yices_model_from_map, which rejects
  function-typed existentials. For a problem with an uninterpreted-function
  existential and arithmetic universals (unsupported by projection-based
  generalization) this is now reported as 'unknown' instead of a fatal bug.

Adds regression test tests/regress/efsmt/ef-tests/iss657.ys.

Coverage Stats

29 of 46 new or added lines in 3 files covered. (63.04%)

1 existing line in 1 file now uncovered.

95573 of 134216 relevant lines covered (71.21%)

1669601.34 hits per line