flyvy-verifier/flyvy

Issues

• Prime missing from mutable axioms in SAT checker

  #158 opened a year ago by edenfrenkel
  3

• Benchmarking infrastructure improvements

  #153 opened a year ago by tchajed
  1

• Proposal for cleaning up Term::Id versus Term::App and the concrete syntax of function calls with zero arguments

  #53 opened 2 years ago by wilcoxjay
  1

• Add documentation for all top-level commands

  #84 opened a year ago by tchajed
  1

• Z3 "incomplete quantifiers" error

  #71 opened a year ago by edenfrenkel
  2

• Add scripts to produce performance benchmarks across all examples

  #118 opened a year ago by tchajed
  3

• Automatically generate and publish the rustdoc docs

  #115 opened a year ago by tchajed
  0

• Refactor out code to get the inits, trs, safes, and axioms from a module

  #102 opened a year ago by Alex-Fischman
  3

• Useless wrapper in verify/error?

  #96 opened a year ago by Alex-Fischman
  1

• Missing documentation for inference and temporal-verifier crates

  #95 opened a year ago by Alex-Fischman
  1

• Replace multi_cartesian_product with a correct version

  #73 opened a year ago by tchajed
  1

• BDD checker should detect convergence

  #89 opened a year ago by wilcoxjay
  0

• Make bdd-check and sat-check have a similar interface to set-check

  #85 opened a year ago by Alex-Fischman
  1

• Create a dummy infer --updr command

  #12 opened a year ago by tchajed
  2

• Z3 timeout during invariant inference

  #68 opened a year ago by edenfrenkel
  2

• Support for more examples

  #70 opened a year ago by edenfrenkel
  2

• running sat sovers with indicator variables produces different results

  #63 opened 2 years ago by oralmer
  2

• Fix substitution in the presence of shadowing global names

  #54 opened 2 years ago by wilcoxjay
  0

• Record timing and solver statistics

  #44 opened 2 years ago by tchajed
  0

• Improve model interpretation performance

  #26 opened 2 years ago by odedp
  0

• Minimize models without evaluating them

  #37 opened 2 years ago by tchajed
  1

• Move houdini flag to infer subcommand

  #11 opened 2 years ago by tchajed
  0

• Add clippy to CI

  #25 opened 2 years ago by wilcoxjay
  3

• Bubble up solver error messages

  #15 opened 2 years ago by tchajed
  1

• Z3 model parsing bug

  #5 opened 2 years ago by edenfrenkel
  1

• Inference is broken using cvc5 with --strict-parsing

  #14 opened 2 years ago by tchajed
  0