epfl-lara/inox

Issues

• Support Scala 2.13

  #100 opened 2 months ago by ptitjes
  0

• Enable reading smt-lib files with dependent types for future text interface from Stainless

  #182 opened 2 years ago by vkuncak
  0

• Add a sequence type: finitary arrays from natural numbers to some type

  #213 opened 3 months ago by vkuncak
  0

• Inox does not compile on Scala 3.3.1 +

  #210 opened 5 months ago by sankalpgambhir
  5

• CVC4/5 unsupported feature shows an error even though another solver is verifying the VC

  #208 opened a year ago by samuelchassot
  2

• Choose under lamba

  #139 opened 3 years ago by jad-hamza
  13

• Migrate to Scala 3.2

  #183 opened 2 years ago by mario-bucev
  1

• StackOverflowError on an equivalence checking example

  #180 opened 3 years ago by drganam
  0

• Underapproximate unfolding

  #169 opened 3 years ago by vkuncak
  0

• ChooseEncoder doesn't transform all the trees

  #167 opened 3 years ago by jad-hamza
  0

• Key not found error when using --debug=tip from Stainless

  #148 opened 3 years ago by jad-hamza
  3

• Integration of `rust-interop` in `master`

  #152 opened 3 years ago by yannbolliger
  0

• Inox error when using set.toList in Stainless

  #117 opened 3 years ago by OStevan
  3

• Type error in tip printed from Stainless

  #153 opened 3 years ago by jad-hamza
  2

• Retrieving defunctionalized string?

  #112 opened 3 years ago by dtwelch
  1

• Mismatch between hasInstance and simplestValue

  #150 opened 3 years ago by jad-hamza
  6

• Code explosion in mergeCalls

  #146 opened 3 years ago by jad-hamza
  3

• Key not found exception on Stainless test case with extern method with quantifiers

  #109 opened 3 years ago by romac
  9

• Missing support for str.++

  #144 opened 3 years ago by jad-hamza
  0

• Parse error with CVC4 1.8

  #110 opened 3 years ago by romac
  3

• Error in documentation when compiling

  #116 opened 3 years ago by OStevan
  6

• Unsat file reported as SAT

  #115 opened 3 years ago by jad-hamza
  2

• NullPointerException with solvers option

  #113 opened 4 years ago by jad-hamza
  1

• Lookup failure in Definitions.scala (line 197), for apply.

  #118 opened 4 years ago by saraswat
  4

• Issue with lambdas and untyped let bindings from Z3 4.8.5

  #104 opened 5 years ago by jad-hamza
  2

• BitVector <-> Integer conversions

  #108 opened 5 years ago by romac
  0

• Inox fails to build because of sbt-tut

  #101 opened 5 years ago by romac
  3

• Error with GADTs and function types

  #93 opened 5 years ago by redelmann
  2

• Error with default parameters in require

  #94 opened 5 years ago by redelmann
  2

• Error in documentation when executing `sbt compile`

  #97 opened 5 years ago by jad-hamza
  2

• Add mode where lambda equality is considered undecidable

  #87 opened 6 years ago by romac
  0

• Inox reports SAT with --feeling-lucky option but UNSAT without

  #83 opened 6 years ago by jad-hamza
  1

• StringSuite test fail with Z3 4.7.1

  #81 opened 6 years ago by jad-hamza
  2

• Two tip files representing the same Stainless VC have a large running time difference

  #80 opened 6 years ago by jad-hamza
  2

• Tests failing with Z3 4.6.0 or newer

  #77 opened 6 years ago by jad-hamza
  5

• Simplification simplifies away (useful) pattern cases

  #78 opened 6 years ago by jad-hamza
  2

• Inox reports an error for invalid (unlucky) models found with `--feeling-lucky`

  #74 opened 6 years ago by romac
  1

• Allow overriding `SymbolTransformer.transform(FunDef)` & co?

  #67 opened 6 years ago by romac
  2

• Symbolic evaluator

  #50 opened 7 years ago by romac
  1

• "String index out of range: 0" in ASCIIStringEncoder

  #58 opened 7 years ago by romac
  2

• Error due to Z3?

  #32 opened 7 years ago by jad-hamza
  17

• Test suite fails with Z3 4.6

  #57 opened 7 years ago by romac
  1

• Purity check

  #37 opened 7 years ago by jad-hamza
  8

• Check behaviour of model with choose

  #30 opened 7 years ago by mantognini
  1

• String newline problem

  #27 opened 7 years ago by MikaelMayer
  3

• String conversion problem

  #24 opened 7 years ago by MikaelMayer
  1

• Z3Optimizer not present in Windows compilation of Inox

  #20 opened 8 years ago by MikaelMayer
  2

• RecursiveEvaluator is wrong for Application

  #17 opened 8 years ago by MikaelMayer
  2

• MatchError: String in SMTLIBTarget

  #15 opened 8 years ago by MikaelMayer
  1

• cons instead of list in the tutorial?

  #11 opened 8 years ago by MikaelMayer
  1