Search results

Tracker for HOL features merged to master

big feature

Status: Open.

#824 In vprover/vampire;

· mezpusz opened on Mar 14, 2026

Sort unification is not done for two variable equalities

Status: Open.

#823 In vprover/vampire;

· mezpusz opened on Mar 14, 2026

memory limit option ignored

Status: Open.

#777 In vprover/vampire;

· easychair opened on Nov 9, 2025

proof checking bug

Status: Open.

#764 In vprover/vampire;

· easychair opened on Sep 23, 2025

Simplify classes that could be implemented with [BottomUp]TermTransformer

Status: Open.

#751 In vprover/vampire;

· mezpusz opened on Aug 6, 2025

Wrong TPTP output for ITE(s) (and possibly other special terms)

Status: Open.

#734 In vprover/vampire;

· mezpusz opened on Jul 16, 2025

Wrong order of quantifiers with type variables

Status: Open.

#733 In vprover/vampire;

· mezpusz opened on Jul 16, 2025

Printing should conform to current output mode

Status: Open.

#731 In vprover/vampire;

· mezpusz opened on Jul 15, 2025

Wrong TPTP output for arithmetic problems

Status: Open.

#730 In vprover/vampire;

· mezpusz opened on Jul 15, 2025

Should use fi_domain and friends.

Status: Open.

#613 In vprover/vampire;

· MichaelRawson opened on Sep 28, 2024

SaturationAlgorithm::addInputSOSClause is currently skipping forwardSimplify

Status: Open.

#562 In vprover/vampire;

· quickbeam123 opened on May 22, 2024

don't synchronise proofs if we don't print them

enhancement

Status: Open.

#548 In vprover/vampire;

· MichaelRawson opened on May 3, 2024