SRI-CSL / yices2

65%

master: 66%

LAST BUILD ON BRANCH fix-mcsat-nira-eq-preprocessing

branch: fix-mcsat-nira-eq-preprocessing

CHANGE BRANCH

x

Reset

• fix-mcsat-nira-eq-preprocessing
• master
• smtcomp-2017
• mcsat-incremental
• v
• Yices-2.5.3
• yices.py
• Yices-2.5.4
• mcsat-bv
• mcsat-nra
• simpler-unsat-cores
• untagged-ccae5cc58023f61e3a62
• Yices-2.6.0
• mcsat-assumptions
• new-bv
• Yices-2.6.1
• case-eval2
• mt-master
• darpa-2019-02-19
• mcsat-model-hint
• mcsat-bv-smtcomp-2019
• fix_array_solver_hash
• 2019-08-19
• 2019-08-19-mcsat-bv
• mcsat-bv-refactorbdds
• size_t
• 2020-02-18
• Yices-2.6.2
• kissat_delegate
• mcsat-nra-intervals
• smtcomp2020
• smt2-output
• valgrind-regress
• mcsat-interpolation
• 2020-08-19
• cross-compile
• mingw-special
• mcsat-eval-2
• 2021-02-19
• definition_clauses
• change_no_error
• smtcomp2021
• mcsat-arrays-2
• unique-fun-decision
• update-weq-term-rep
• mcsat-array-comb
• weq-fix-todo
• array-tests
• mcsat-keep-binary-clauses
• bool-bump-factor
• mcsat-imp-reducedb
• mcsat-array-patch-1
• iss440-fix
• mcsat-array-finite
• mcsat-array-sort-heuristic
• qf-eq-bv-arith
• fix-array-model-print-smt2
• refs/heads/mcsat_uf_model_fix
• mcsat-arrays-fix
• mcsat_uf_model_fix
• 393-api-could-yices_assert_blocking_clause-return-the-clause
• update-html-doc
• fix-strerror-mingw
• fix-timeout-mingw
• win-ci
• ahmed-irfan-patch-1
• win-ci-2
• rename-smt-status-enum
• patch-iss-418-prerelease
• update-ci
• update-win-ci-thread-safety
• mcsat-array-learn
• mcsat-check-model-with-hint
• fix-compilation-warnings
• rm-scratch-compilation
• test-var-order
• mcsat-api-var-order
• mcsat-model-hint-registration-queue-fix
• update-set-var-oder-api
• tmp_good
• mcsat-filter-binary-clauses
• mcsat-lemma-limit-update
• mcsat-glue-reduce
• mcsat-array-simplify-var-bump
• update-ci-check-api
• fix-check-api-warning
• update-actions-checkout-4
• mcsat-bv-array-purify
• mcsat-learn
• mcsat-arrays-fixes
• mcsat-set-initial-var-order-api
• mcsat-array-improved-call
• 486-assertion-failure-in-srcmcsatvaluec-could-be-a-duplicate-of-451
• test-451
• mcsat-update-heuristic
• test-initial-order
• fix-interpolant-with-empty-model
• nra-learn-hint-next-decision
• mcsat-recache
• mcsat-int-hint-2
• bvlra
• hint-real-decisions
• smtcomp2024
• mcsat-ufnra-model-fix
• 2.6.5
• refs/tags/Yices-2.6.5
• rand-cmd
• fix-unit-tests
• ci-make-test
• smt2-set-option-timeout
• mcsat-new-reduce
• nra-cached-must-decide
• mcsat-target
• reintroduce-interval-approx-nra
• mcsat-target-best

Build # 7052650242

Build Type

Pull #481

github

Committed by web-flow

Commit Message

Merge 424c00633 into f1860fe25

Pull Request Pull Request #481: MCSAT: Preprocessor: fix equality simplification for mixed real-integer terms

Run Details

3 of 3 new or added lines in 1 file covered. (100.0%)

79302 of 121739 relevant lines covered (65.14%)

1507560.87 hits per line