mtrberzi/z3

Issues

• Difference in running time depending on string literals

  #37 opened 7 years ago
  1

• regex_automata sat-as-unsat z3str/regex-010.smt2

  #36 opened 7 years ago
  0

• Z3prover/Z3 #748: possible sat-as-unsat?

  #35 opened 7 years ago
  1

• Z3 master uses "seq" as default string solver option

  #34 opened 7 years ago
  0

• unhandled cases in binary search

  #33 opened 8 years ago
  0

• make better use of trail stack in pop_scope_eh and related

  #32 opened 8 years ago
  0

• use expr_ref_vector instead of std::vector wherever possible

  #31 opened 8 years ago
  0

• improved data structure for contain_pair_idx_map

  #30 opened 8 years ago
  0

• expr* to expr_ref refactoring wherever possible

  #29 opened 8 years ago
  0

• str_rewriter reduce_eq

  #28 opened 8 years ago
  0

• Behaviour of leading zeroes in string-integer conversion

  #27 opened 8 years ago
  0

• examples and test cases for C API

  #26 opened 8 years ago
  0

• scope handling wrt. indexof2-006.smt2

  #25 opened 8 years ago
  0

• performance: regex-023 and regex-026

  #24 opened 8 years ago
  0

• proper parameters module

  #23 opened 8 years ago
  0

• support for higher-level regex operators

  #22 opened 8 years ago
  0

• Handling of \"

  #21 opened 8 years ago
  1

• regression: tests/z3str/replace-001.smt2

  #20 opened 8 years ago
  0

• regression: tests/z3str/substring-001.smt2

  #19 opened 8 years ago
  0

• change term-specific axiom todo lists into a generic library_aware_axiom_todo list

  #18 opened 8 years ago
  0

• check whether we need to set up axioms on terms generated by setting up axioms

  #17 opened 8 years ago
  0

• investigate crashes/segfaults related to Indexof

  #16 opened 8 years ago
  0

• fast Contains checks

  #15 opened 8 years ago
  0

• support for Contains

  #14 opened 8 years ago
  0

• support for SubStr

  #13 opened 8 years ago
  1

• support for StartsWith

  #12 opened 8 years ago
  0

• support for Replace

  #11 opened 8 years ago
  1

• support for LastIndexOf

  #10 opened 8 years ago
  1

• support for IndexOf2

  #9 opened 8 years ago
  1

• support for IndexOf

  #8 opened 8 years ago
  1

• support for EndsWith

  #7 opened 8 years ago
  0

• support for CharAt

  #6 opened 8 years ago
  0

• regression: tests/z3str/concat-064.smt2

  #5 opened 8 years ago
  0

• (Length x) as an arithmetic theory variable?

  #4 opened 8 years ago
  0

• use m_strutil.get_const_string_value() to extract a string constant into a std::string

  #3 opened 8 years ago
  0

• concat-eq-concat processing fails due to assertion violation

  #2 opened 9 years ago
  1

• theory of arithmetic isn't being loaded properly

  #1 opened 9 years ago
  0