VeriFIT/z3-noodler

Issues

• Incorrect result

  #135 opened 2 months ago by jurajsic
  1

• Unify variable creation

  #86 opened 2 months ago by vhavlena
  3

• Bug for not contains

  #157 opened 3 months ago by jurajsic
  2

• Determinization argument in `regex::conv_to_nfa` is not passed for concatenation

  #155 opened 4 months ago by jurajsic
  0

• Error in Installing

  #127 opened 7 months ago by AnkitMU
  14

• Move rules from predicate axiomatization to theory rewriter

  #122 opened 8 months ago by vhavlena
  1

• Representation of `notconstains` and `to_int`/`from_int` in Formula

  #119 opened 8 months ago by vhavlena
  0

• Add a basic support for `to_int`/`from_int`

  #76 opened 9 months ago by vhavlena
  0

• Automata in noodles are not reduced

  #106 opened 10 months ago by jurajsic
  1

• Add support for `str.<` and `str.<=`

  #84 opened a year ago by jurajsic
  0

• Support for `replace_re`

  #75 opened a year ago by vhavlena
  1

• Update install information

  #92 opened a year ago by vhavlena
  4

• Support for `seq.unit`

  #95 opened a year ago by vhavlena
  0

• Update to the current version of `mata`

  #91 opened a year ago by vhavlena
  0

• Create a dispatcher for different decision procedures

  #79 opened a year ago by vhavlena
  0

• Specific predicate instances

  #77 opened a year ago by vhavlena
  0

• Too defensive `contains` handling

  #85 opened a year ago by jurajsic
  0

• Function comments in headers vs source files

  #90 opened a year ago by jurajsic
  0

• Refactoring of the theory core

  #73 opened a year ago by vhavlena
  0

• Rewriting string rewriter

  #83 opened a year ago by jurajsic
  1

• Regex construction optimization

  #81 opened a year ago by vhavlena
  0

• Quadratic equations

  #74 opened a year ago by vhavlena
  1

• Correctly determine whether `expr` is a variable

  #20 opened a year ago by Adda0
  0

• Return `unknown` for difficult predicates

  #27 opened a year ago by vhavlena
  0

• Fresh literal

  #41 opened 2 years ago by vhavlena
  0

• IntAlphabet in automata assignment

  #40 opened 2 years ago by vhavlena
  2

• Support for inequalities

  #26 opened 2 years ago by vhavlena
  0

• Add visualization of inclusion graphs

  #30 opened 2 years ago by vhavlena
  0

• Check that we are able to solve `re.replace`

  #21 opened 2 years ago by Adda0
  1

• Substring bug

  #10 opened 2 years ago by vhavlena
  0