SRI-CSL/sally

Issues

• Requirements for CUDD not documented

  #70 opened 8 months ago by TomMD
  0

• About available first-order logic semantics.

  #65 opened 5 years ago by zqzqz
  1

• Trouble verifying "weakend" properties

  #61 opened 5 years ago by yav
  0

• Using `mod` with `mcmt`

  #60 opened 6 years ago by yav
  0

• Yices2-mcsat and converting between Real and Integer

  #58 opened 6 years ago by yav
  0

• Integer division?

  #57 opened 6 years ago by yav
  0

• Missing `floor` function?

  #56 opened 6 years ago by yav
  1

• Failing tests when building

  #55 opened 6 years ago by delenius
  1

• Surprising behavior when using `pdkind`

  #54 opened 6 years ago by yav
  1

• Yices error when invoking sally

  #53 opened 6 years ago by yav
  2

• Segfaults

  #50 opened 6 years ago by yav
  3

• Parse the SyGuS competition format

  #38 opened 8 years ago by dddejan
  0

• Improve integer reasoning

  #39 opened 8 years ago by dddejan
  0

• "Variable not part of model" when showing trace

  #52 opened 6 years ago by yav
  1

• Incorrect traces, depending on the order of queries

  #51 opened 6 years ago by yav
  2

• Suggestions on input format

  #49 opened 7 years ago by aman-goel
  1

• Some weird error with regression test `pdkind/example9.mcmt` in debug mode

  #48 opened 7 years ago by caballa
  3

• Add sally to our Homebrew Tap

  #47 opened 7 years ago by ianamason
  1

• Parse errors

  #46 opened 7 years ago by rainoftime
  2

• Finish bit-vector parsing

  #20 opened 7 years ago by dddejan
  0

• C++ API for sally?

  #44 opened 7 years ago by rainoftime
  1

• Doesn't work with clang

  #26 opened 8 years ago by dddejan
  2

• trace generation for ic3

  #34 opened 8 years ago by dddejan
  1

• Integrate crab into Sally

  #42 opened 8 years ago by dddejan
  1

• Add learned invariants to IC3

  #43 opened 8 years ago by dddejan
  0

• Z3 mystery

  #41 opened 8 years ago by ianamason
  3

• sally needs to be noticed.

  #40 opened 8 years ago by ianamason
  5

• cryptic yices error

  #33 opened 8 years ago by xapantu
  2

• Fix OCaml build in frontend/apron

  #36 opened 8 years ago by dddejan
  1

• Abstraction infinite loop

  #37 opened 8 years ago by dddejan
  0

• typecheck error in a file with multiple queries

  #32 opened 8 years ago by xapantu
  1

• Add parsers for aiger

  #14 opened 8 years ago by dddejan
  0

• segfault when asking to show the trace

  #31 opened 8 years ago by xapantu
  1

• Unable to use escaped ids

  #28 opened 9 years ago by agacek
  3

• btor bmc tests failing on ubuntu 15.10

  #27 opened 9 years ago by dddejan
  2

• Feature request: Multiple engines

  #29 opened 9 years ago by agacek
  2

• Multi-property solving

  #30 opened 9 years ago by agacek
  2

• Add input type as part of transitions

  #22 opened 9 years ago by dddejan
  0

• Failure in yices model construction.

  #25 opened 9 years ago by dddejan
  1

• Finish garbage-collection

  #24 opened 10 years ago by dddejan
  0

• Allow inline definitions of the transition system

  #19 opened 10 years ago by dddejan
  1

• Setup build configuration to check for solver versions

  #21 opened 10 years ago by dddejan
  2

• Assertion failure in Yices

  #23 opened 10 years ago by dddejan
  2

• Output counter-examples for IC3

  #17 opened 10 years ago by dddejan
  0

• Output invariant for IC3

  #18 opened 10 years ago by dddejan
  0

• Add transitions as let, and add 'cond' operator

  #16 opened 10 years ago by dddejan
  0

• Fix integer/real typechecking

  #15 opened 10 years ago by dddejan
  0

• Implement model-extraction from SMT solvers

  #13 opened 10 years ago by dddejan
  0

• add smt2 generic solver

  #11 opened 10 years ago by dddejan
  1

• fix valgrind forblems with yices interface

  #12 opened 10 years ago by dddejan
  1