Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Jan 20, 2016

• fix warning message for unused variable

  Show description for 993a043
  NikolajBjorner

  committed
  993a043

  Copy full SHA for 993a043

Commits on Jan 19, 2016

• Merge branch 'master' of https://github.com/Z3Prover/z3

  NikolajBjorner

  committed
  099e572

  Copy full SHA for 099e572

• make parse error a bit more informative

  Show description for a021e51
  NikolajBjorner

  committed
  a021e51

  Copy full SHA for a021e51

• remove m_ast_lim from API context since that one isn't used either

  Show description for 23cc825
  nunoplopes

  committed
  23cc825

  Copy full SHA for 23cc825

• remove m_replay_stack from API context since it's never used

  Show description for 1f872e7
  nunoplopes

  committed
  1f872e7

  Copy full SHA for 1f872e7

• Merge branch 'master' of https://github.com/Z3Prover/z3

  NikolajBjorner

  committed
  d9e4648

  Copy full SHA for d9e4648

• bug-fixes to sequence theory

  Show description for cccd502
  NikolajBjorner

  committed
  cccd502

  Copy full SHA for cccd502

Commits on Jan 18, 2016

• Efficiency fix for fp.div.

  

  Christoph M. Wintersteiger

  committed
  4dba527

  Copy full SHA for 4dba527

• Bugfix for FP model converter.

  

  Christoph M. Wintersteiger

  committed
  99176cc

  Copy full SHA for 99176cc

• fix axiomatization for at

  Show description for c9373eb
  NikolajBjorner

  committed
  c9373eb

  Copy full SHA for c9373eb

• Merge branch 'master' of https://github.com/Z3Prover/z3

  NikolajBjorner

  committed
  6aed3c3

  Copy full SHA for 6aed3c3

• fix axioms for extract, add extensionality checking for shared variables, convert exceptions to unknown status per Z3Prover#419

  Show description for 85d44c5
  NikolajBjorner

  committed
  85d44c5

  Copy full SHA for 85d44c5

Commits on Jan 17, 2016

• Undid previous update of SMT2 scanner to support the new SMT2.5 string escaping.

  

  Christoph M. Wintersteiger

  committed
  99d2ab4

  Copy full SHA for 99d2ab4

Commits on Jan 16, 2016

• Fix for escape sequences in SMT2 scanner

  

  Christoph M. Wintersteiger

  committed
  01cb20e

  Copy full SHA for 01cb20e

Commits on Jan 15, 2016

• fix bugs in sequence extraction from NFA

  Show description for 88362a1
  NikolajBjorner

  committed
  88362a1

  Copy full SHA for 88362a1

• add parameter validation to sequence expressions

  Show description for 14c19fe
  NikolajBjorner

  committed
  14c19fe

  Copy full SHA for 14c19fe

• update re simplification

  Show description for 150c5c2
  NikolajBjorner

  committed
  150c5c2

  Copy full SHA for 150c5c2

Commits on Jan 14, 2016

• add seq_rewriter to model_evaluator, remove th_rewriter additional step in validator

  Show description for a295dd4
  NikolajBjorner

  committed
  a295dd4

  Copy full SHA for a295dd4

• enhance model validation to invoke rewriter if result isn't true using the simplify-based model evaluator

  Show description for 7cbd59b
  NikolajBjorner

  committed
  7cbd59b

  Copy full SHA for 7cbd59b

• fix tout -> out. Tune generation of automata transitions

  Show description for 01fd3c9
  NikolajBjorner

  committed
  01fd3c9

  Copy full SHA for 01fd3c9

• fix tout -> out. Tune generation of automata transitions

  Show description for 2d41b0e
  NikolajBjorner

  committed
  2d41b0e

  Copy full SHA for 2d41b0e

• Debug-fix for theory_seq. Fixes Z3Prover#418.

  

  Christoph M. Wintersteiger

  committed
  0f08257

  Copy full SHA for 0f08257

• fix back rewriting for concat

  Show description for 3ff9735
  NikolajBjorner

  committed
  3ff9735

  Copy full SHA for 3ff9735

• add support for re.nostr, re.all, fix bug in disequality handling of sequences, update signature of loop to handle integer arguments and variable arguments

  Show description for de9c959
  NikolajBjorner

  committed
  de9c959

  Copy full SHA for de9c959

Commits on Jan 13, 2016

• fix build

  Show description for a81c7c4
  NikolajBjorner

  committed
  a81c7c4

  Copy full SHA for a81c7c4

• Merge branch 'master' of https://github.com/Z3Prover/z3

  NikolajBjorner

  committed
  2f0a049

  Copy full SHA for 2f0a049

• add empty/full regular languages, escape sequence fixes, check cancellation inside simplifier

  Show description for e021540
  NikolajBjorner

  committed
  e021540

  Copy full SHA for e021540

• Changed FP significand/exponent functions to return non-normalized results. Clarified function remarks. Relates to Z3Prover#383.

  

  Christoph M. Wintersteiger

  committed
  357ec9e

  Copy full SHA for 357ec9e

• Merge pull request Z3Prover#409 from delcypher/ml_respect_destdir

  Show description for e0f873c
  

  Christoph M. Wintersteiger

  committed
  e0f873c

  Copy full SHA for e0f873c

• model generation with strings

  Show description for 57e1d4d
  NikolajBjorner

  committed
  57e1d4d

  Copy full SHA for 57e1d4d

• add range / loop handling for re. Fix regression reading mixed numerals reported by Trentin

  Show description for 9909c05
  NikolajBjorner

  committed
  9909c05

  Copy full SHA for 9909c05

Commits on Jan 12, 2016

• re-enable feature that lets Z3 solver mixed integer/real constraints with additional information tha texpressions with sort real can only take integer values. Fixes regression on epsilon.smt2

  Show description for 9a6fe93
  NikolajBjorner

  committed
  9a6fe93

  Copy full SHA for 9a6fe93

• revert mixed integer/real handling pending fix to equality propagation

  Show description for e2d5494
  NikolajBjorner

  committed
  e2d5494

  Copy full SHA for e2d5494

• Fix bug when configuring when building OCaml bindings is enabled

  Show description for 250c8d0
  

  Dan Liew

  committed
  250c8d0

  Copy full SHA for 250c8d0

• Merge branch 'master' of https://github.com/Z3Prover/z3

  NikolajBjorner

  committed
  f897136

  Copy full SHA for f897136

Pagination

Previous

Next