vprover/vampire

Issues

• FOOL constant symbol assertion violation

  #606 opened 2 months ago by mezpusz
  2

• Well-sortedness check fails during preprocessing in ITP206_4

  #602 opened 3 months ago by mezpusz
  1

• Assertion violation with $let sorts

  #604 opened 2 months ago by mezpusz
  1

• Reduce reliance on platform-specific APIs, improve Windows support

  #462 opened a year ago by MichaelRawson
  4

• UWA test fails on linux build

  #590 opened 3 months ago by Angular-Angel
  17

• Aligned allocation is broken: `error: 'aligned_alloc' is not a member of 'std'; did you mean 'aligned_union'?`

  #592 opened 3 months ago by barracuda156
  3

• Distinct domain constants with the same name.

  #478 opened 3 months ago by MichaelRawson
  1

• No undefined symbols in finite models.

  #477 opened 3 months ago by MichaelRawson
  1

• A different operator precedence when parsing HOL?

  #553 opened 5 months ago by quickbeam123
  1

• bad test id errors

  #576 opened 5 months ago by joe-hauns
  1

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

  #548 opened 7 months ago by MichaelRawson
  1

• Printing some large proofs kills us?

  #567 opened 6 months ago by quickbeam123
  2

• How make Vampire return true/false for a given problem (question)?

  #560 opened 6 months ago by k00ni
  5

• Crash on `PUZ091^5` with NewCNF

  #556 opened 7 months ago by MichaelRawson
  4

• No proof with implies-transitive SMT problem (regression)

  #563 opened 6 months ago by kazarmy
  4

• UPDR incorrect (deletes too much) in the presence of specially parsed function definitions from SMT

  #561 opened 6 months ago by quickbeam123
  4

• Vampire crashing when printing a finite model:

  #565 opened 6 months ago by quickbeam123
  1

• SaturationAlgorithm::addInputSOSClause is currently skipping forwardSimplify

  #562 opened 6 months ago by quickbeam123
  0

• Bad saturation on `SYO500_8.008`

  #557 opened 6 months ago by MichaelRawson
  11

• Polymorphism and Z3 not playing nicely

  #453 opened 6 months ago by ibnyusuf
  5

• Parse errors for polymorphic problems

  #415 opened 7 months ago by ibnyusuf
  4

• FDI is really not very good and not type-safe.

  #555 opened 7 months ago by MichaelRawson
  0

• Miscellanious Crashes

  #542 opened 7 months ago by joe-hauns
  14

• Reimplement Lib/Set.hpp as a wrapper of std::unordered_set

  #551 opened 7 months ago by inpefess
  9

• Properly parenthesise function declarations in TPTP output

  #476 opened 7 months ago by MichaelRawson
  1

• Duplicate 'finite_domain' axiom names in TPTP models

  #475 opened 7 months ago by MichaelRawson
  1

• Properly quote axiom names in TPTP solutions

  #474 opened 7 months ago by MichaelRawson
  1

• Unexpected "User error: This version cannot be used with this logic!"

  #550 opened 7 months ago by ibnyusuf
  1

• Do not report builtin sorts in TPTP models.

  #473 opened 7 months ago by MichaelRawson
  0

• 3 tests fail on Sonoma / aarch64

  #545 opened 8 months ago by barracuda156
  3

• [macOS] Build uses unsupported flags which break it: `cc1plus: error: '-fno-fat-lto-objects' are supported only with linker plugin`

  #512 opened 8 months ago by barracuda156
  40

• Linking error when building Debug version in Cygwin

  #519 opened 10 months ago by inpefess
  8

• Revive `gcov`

  #516 opened 10 months ago by inpefess
  2

• Smart ep=RSTC skips congruences for introduced symbols for which it shouldn't?

  #509 opened a year ago by quickbeam123
  2

• RobSubstitution::match is unsound

  #445 opened 2 years ago by ibnyusuf
  4

• The version of z3 we are currently linking against (tag: z3-4.12.2 from May) again fails to deliver definite answers sometimes

  #503 opened a year ago by quickbeam123
  3

• Some useless congruence axioms by equality proxy under arithmetic inputs

  #501 opened a year ago by quickbeam123
  0

• performance regression?

  #482 opened a year ago by apease
  6

• Use-after-free in proof printing.

  #465 opened a year ago by MichaelRawson
  4

• `(expt 2 8)` induction?

  #448 opened a year ago by kazarmy
  7

• Skolem type in same block as term causes assertion violation.

  #421 opened a year ago by MichaelRawson
  10

• Crash on model output from FMB - sorts?

  #461 opened a year ago by MichaelRawson
  1

• Incorrect saturations for problems containing FOOL

  #454 opened a year ago by ibnyusuf
  4

• Time-out with satisfiable problems in SMT-LIB2

  #446 opened 2 years ago by KJanelle
  2

• Lost sort information in quantifier blocks causes problems later.

  #440 opened 2 years ago by MichaelRawson
  0

• Question about bitvector

  #430 opened 2 years ago by TraceShadow
  2

• Question answering

  #434 opened 2 years ago by stanmoon
  10

• Hey

  #427 opened 2 years ago by Hiireen1981
  0

• Hey

  #428 opened 2 years ago by Hiireen1981
  0

• Imperfect Filtering

  #408 opened 2 years ago by ibnyusuf
  8