nunchaku-inria nunchaku issues

nunchaku-inria / nunchaku

Model finder for higher-order logic

https://nunchaku-inria.github.io/nunchaku/

BSD 2-Clause "Simplified" License

41 stars 3 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Release page returns 403 error, and compiling nunchaku fails with numerous errors

#37 nano-o opened 1 year ago
3
README references missing files

#36 maxvonhippel closed 3 years ago
1
Parse error on TIP input

#35 mikkelmilo opened 4 years ago
6
nunchaku on continuous functions on codatatypes in Isabelle

#34 singhjagadish opened 4 years ago
3
Can't find nun-file after using nunchaku in isabelle

#33 singhjagadish opened 5 years ago
1
polymorphic constants

#32 c-cube opened 5 years ago
0
Avoid using a wildcard in a Menhir production.

#31 fpottier closed 5 years ago
1
Could nunchaku be used for Coq (which allows empty types)?

#30 samuelgruetter opened 5 years ago
0
nunchaku fails to find a counterexample for a simple list-based map implementation

#29 samuelgruetter opened 5 years ago
3
Type error without line number

#28 samuelgruetter closed 5 years ago
2
CVC4 1.7 support

#27 samuelgruetter closed 5 years ago
2
opam installation failed for OCaml 4.03.0

#26 samuelgruetter closed 5 years ago
5
warning for partially defined functions

#25 c-cube opened 6 years ago
0
bug: match cases need type arguments

#24 c-cube closed 5 years ago
0
approximate quantifiers in `ElimData` on incomplete types

#23 c-cube closed 6 years ago
1
improve cardinality analysis for kodkod

#22 c-cube closed 7 years ago
1
fix release 0.4 for win32

#21 c-cube closed 7 years ago
0
support for dependent types

#20 c-cube opened 7 years ago
0
inlining pass

#19 c-cube opened 7 years ago
0
add prototypes

#18 c-cube opened 7 years ago
0
Unclear error if backend solver is not installed

#17 blanchette closed 7 years ago
0
keep definition of alpha_u even when unused

#16 ML44 closed 7 years ago
0
Type error : remaining meta-variable

#15 ML44 closed 8 years ago
0
CVC4 bug NodeValue

#14 ML44 closed 8 years ago
1
Alarm clock 14

#13 ML44 closed 8 years ago
1
Better error message when pred not well funded.

#12 ML44 closed 8 years ago
0
in skolem, ignore `let`-bound variables

#11 c-cube closed 7 years ago
1
better parsing of CVC4

#10 c-cube closed 8 years ago
0
cleanup duplicates in models

#9 c-cube closed 8 years ago
0
cardinality bounds

#8 c-cube closed 8 years ago
0
modify syntax for `spec`

#7 c-cube closed 8 years ago
1
use 0-cardinality sorts

#6 c-cube opened 8 years ago
0
transformation for introducing destructors

#5 c-cube opened 8 years ago
0
(co)inductive predicates

#4 c-cube closed 8 years ago
1
precedence-based printers

#3 c-cube closed 7 years ago
0
add an `include` statement

#2 c-cube closed 8 years ago
1
support partially applied builtins

#1 c-cube closed 8 years ago
0