uclid-org/uclid

Issues

• Bug in RewritePolymorphicSelect

  #249 opened 6 months ago by FedericoAureliano
  1

• Bit-vector arithmetic questions

  #258 opened 6 months ago by ulysse-lh
  2

• Tester application without argument causes crash

  #250 opened 6 months ago by FedericoAureliano
  0

• SMTLIB declaration dependencies ignored

  #255 opened 6 months ago by FedericoAureliano
  0

• ADT Type Confusion

  #253 opened 6 months ago by FedericoAureliano
  0

• Type Checking with ADTs

  #242 opened 6 months ago by FedericoAureliano
  0

• `generateDatatype` does not generate inner types for ADTs

  #245 opened 6 months ago by adwait
  0

• ADT is facing some canonicalization issue during module instantiation

  #248 opened 8 months ago by adwait
  0

• Can an ADT reuse same field names for different constructors?

  #246 opened 8 months ago by adwait
  1

• Unsimplified SynonymType in DataType

  #244 opened 8 months ago by adwait
  1

• instance procedure calls use modified values

  #156 opened 3 years ago by adwait
  1

• ADT TODOs

  #240 opened 8 months ago by polgreen
  0

• Counterexample doesn't make sense

  #207 opened a year ago by tommy11jo
  3

• Simple liveness checks incorrectly passing

  #206 opened 2 years ago by AnimeshAgrawal
  1

• RewriteRecordSelect conflicts with printing individual fields in counterexamples

  #202 opened 2 years ago by adwait
  5

• Record Rewriter's Bugs

  #200 opened 2 years ago by lichye
  0

• SExpr parser/parsing models

  #98 opened 2 years ago by polgreen
  0

• Different verification results produced when there is only a variable name difference

  #198 opened 2 years ago by zpzigi754
  4

• TODO: printing of enums in synth functions

  #197 opened 2 years ago by polgreen
  0

• error splitting commands

  #191 opened 2 years ago by polgreen
  1

• tutorial/ex4.4 embeded assertions not working as expected

  #169 opened 2 years ago by kofyou
  2

• The `bmc` command currently ignores `assert` statements.

  #181 opened 2 years ago by lsk567
  1

• Assumption on array causes malfunctioning checks

  #173 opened 3 years ago by kofyou
  5

• Assertions on values of variables changed by child modules in `next` block have inconsistent values

  #163 opened 3 years ago by noloerino
  0

• Variables sometimes fail to update in counterexamples

  #160 opened 3 years ago by noloerino
  3

• Z3 array not converted to string in counterexample

  #159 opened 3 years ago by noloerino
  2

• Enum variants in modules not recognized without importing type in main module

  #154 opened 3 years ago by noloerino
  1

• Record literals not type-checking properly

  #155 opened 3 years ago by noloerino
  0

• synthesis test 7

  #152 opened 3 years ago by polgreen
  0

• synthesis test 7

  #151 opened 3 years ago by polgreen
  0

• TODO: add travis CI to PR checks

  #39 opened 3 years ago by polgreen
  1

• enum pass bugs

  #87 opened 4 years ago by polgreen
  1

• TODO: document finite_foralls

  #123 opened 3 years ago by polgreen
  1

• using past and history function in invariants

  #145 opened 3 years ago by sderrien
  3

• The counterexample of induction with k > 1 shows one less state in the induction_step.

  #143 opened 3 years ago by lsk567
  1

• bmc should not ignore non-LTL properties

  #64 opened 3 years ago by polgreen
  0

• LTL bug

  #128 opened 3 years ago by polgreen
  0

• TODO: macros

  #117 opened 3 years ago by polgreen
  0

• replace genericProofCommand

  #116 opened 3 years ago by polgreen
  0

• chaining of multiply needs parentheses

  #96 opened 4 years ago by polgreen
  0

• bitwise operations on integers cause uncaught exceptions

  #106 opened 4 years ago by Smattr
  1

• parsing of record field names that collide with variable names

  #99 opened 4 years ago by Smattr
  4

• z3 java bindings on Mac

  #105 opened 4 years ago by polgreen
  0

• CI: add CVC4

  #45 opened 4 years ago by ekiwi
  3

• Typo in https://github.com/uclid-org/uclid/blob/master/mac-install.md

  #89 opened 4 years ago by aayan636
  1

• upgrade SBT

  #79 opened 4 years ago by polgreen
  0

• parsing check: print cex doesn't check if variable is defined

  #74 opened 4 years ago by polgreen
  1

• [request] will UCLID support a division operator?

  #68 opened 4 years ago by sxysun-zz
  2

• fix and re-enable redundant assignment eliminator

  #59 opened 4 years ago by polgreen
  1

• TODO: change inlining semantics

  #42 opened 4 years ago by polgreen
  1