package yices2

  1. Overview
  2. Docs
type code =
  1. | NO_ERROR
  2. | INVALID_TYPE
  3. | INVALID_TERM
  4. | INVALID_CONSTANT_INDEX
  5. | INVALID_VAR_INDEX
  6. | INVALID_TUPLE_INDEX
  7. | INVALID_RATIONAL_FORMAT
  8. | INVALID_FLOAT_FORMAT
  9. | INVALID_BVBIN_FORMAT
  10. | INVALID_BVHEX_FORMAT
  11. | INVALID_BITSHIFT
  12. | INVALID_BVEXTRACT
  13. | INVALID_BITEXTRACT
  14. | TOO_MANY_ARGUMENTS
  15. | TOO_MANY_VARS
  16. | MAX_BVSIZE_EXCEEDED
  17. | DEGREE_OVERFLOW
  18. | DIVISION_BY_ZERO
  19. | POS_INT_REQUIRED
  20. | NONNEG_INT_REQUIRED
  21. | SCALAR_OR_UTYPE_REQUIRED
  22. | FUNCTION_REQUIRED
  23. | TUPLE_REQUIRED
  24. | VARIABLE_REQUIRED
  25. | ARITHTERM_REQUIRED
  26. | BITVECTOR_REQUIRED
  27. | SCALAR_TERM_REQUIRED
  28. | WRONG_NUMBER_OF_ARGUMENTS
  29. | TYPE_MISMATCH
  30. | INCOMPATIBLE_TYPES
  31. | DUPLICATE_VARIABLE
  32. | INCOMPATIBLE_BVSIZES
  33. | EMPTY_BITVECTOR
  34. | ARITHCONSTANT_REQUIRED
  35. | INVALID_MACRO
  36. | TOO_MANY_MACRO_PARAMS
  37. | TYPE_VAR_REQUIRED
  38. | DUPLICATE_TYPE_VAR
  39. | BVTYPE_REQUIRED
  40. | BAD_TERM_DECREF
  41. | BAD_TYPE_DECREF
  42. | INVALID_TOKEN
  43. | SYNTAX_ERROR
  44. | UNDEFINED_TYPE_NAME
  45. | UNDEFINED_TERM_NAME
  46. | REDEFINED_TYPE_NAME
  47. | REDEFINED_TERM_NAME
  48. | DUPLICATE_NAME_IN_SCALAR
  49. | DUPLICATE_VAR_NAME
  50. | INTEGER_OVERFLOW
  51. | INTEGER_REQUIRED
  52. | RATIONAL_REQUIRED
  53. | SYMBOL_REQUIRED
  54. | TYPE_REQUIRED
  55. | NON_CONSTANT_DIVISOR
  56. | NEGATIVE_BVSIZE
  57. | INVALID_BVCONSTANT
  58. | TYPE_MISMATCH_IN_DEF
  59. | ARITH_ERROR
  60. | BVARITH_ERROR
  61. | CTX_FREE_VAR_IN_FORMULA
  62. | CTX_LOGIC_NOT_SUPPORTED
  63. | CTX_UF_NOT_SUPPORTED
  64. | CTX_ARITH_NOT_SUPPORTED
  65. | CTX_BV_NOT_SUPPORTED
  66. | CTX_ARRAYS_NOT_SUPPORTED
  67. | CTX_QUANTIFIERS_NOT_SUPPORTED
  68. | CTX_LAMBDAS_NOT_SUPPORTED
  69. | CTX_NONLINEAR_ARITH_NOT_SUPPORTED
  70. | CTX_FORMULA_NOT_IDL
  71. | CTX_FORMULA_NOT_RDL
  72. | CTX_TOO_MANY_ARITH_VARS
  73. | CTX_TOO_MANY_ARITH_ATOMS
  74. | CTX_TOO_MANY_BV_VARS
  75. | CTX_TOO_MANY_BV_ATOMS
  76. | CTX_ARITH_SOLVER_EXCEPTION
  77. | CTX_BV_SOLVER_EXCEPTION
  78. | CTX_ARRAY_SOLVER_EXCEPTION
  79. | CTX_INVALID_OPERATION
  80. | CTX_OPERATION_NOT_SUPPORTED
  81. | CTX_INVALID_CONFIG
  82. | CTX_UNKNOWN_PARAMETER
  83. | CTX_INVALID_PARAMETER_VALUE
  84. | CTX_UNKNOWN_LOGIC
  85. | EVAL_UNKNOWN_TERM
  86. | EVAL_FREEVAR_IN_TERM
  87. | EVAL_QUANTIFIER
  88. | EVAL_LAMBDA
  89. | EVAL_OVERFLOW
  90. | EVAL_FAILED
  91. | EVAL_CONVERSION_FAILED
  92. | EVAL_NO_IMPLICANT
  93. | MDL_UNINT_REQUIRED
  94. | MDL_CONSTANT_REQUIRED
  95. | MDL_DUPLICATE_VAR
  96. | MDL_FTYPE_NOT_ALLOWED
  97. | MDL_CONSTRUCTION_FAILED
  98. | YVAL_INVALID_OP
  99. | YVAL_OVERFLOW
  100. | OUTPUT_ERROR
  101. | INTERNAL_EXCEPTION
type report = {
  1. name : string;
  2. line : int;
  3. column : int;
  4. term1 : term option;
  5. type1 : typ option;
  6. term2 : term option;
  7. type2 : typ option;
  8. badval : int64;
}
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct