3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-21 16:16:38 +00:00
z3/src
Nikolaj Bjorner 74292a48e5 change order of concatentation for empty string, #1595
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-26 09:08:34 +02:00
..
ackermannization Use nullptr. 2018-02-12 14:05:55 +07:00
api adding the orphaned shorthand #1574 2018-04-13 23:10:21 -07:00
ast change order of concatentation for empty string, #1595 2018-04-26 09:08:34 +02:00
cmd_context fix #1575, fix #1585 2018-04-23 07:11:15 +02:00
duality Use nullptr. 2018-02-12 14:05:55 +07:00
interp fix #1547 by rewriting legacy recognizers to SMT-LIB2.6 style recognizers which are assumed by theory_datatype 2018-03-19 13:33:58 -07:00
math Remove int64, uint64 typedefs in favor of int64_t / uint64_t. 2018-03-31 14:45:04 +07:00
model fix #1567 2018-04-08 11:19:00 -07:00
muz fix #1592 #1587 2018-04-25 11:18:24 +02:00
nlsat Use nullptr. 2018-02-12 14:05:55 +07:00
opt add warning message for optimization with quantifiers. Fix #1580 2018-04-23 07:20:24 +02:00
parsers enable patterns on equality, add trace for variables for axiom profiling. 2018-04-20 11:44:30 +03:00
qe Remove int64, uint64 typedefs in favor of int64_t / uint64_t. 2018-03-31 14:45:04 +07:00
sat don't reinit assumptions when the solver is unsat. fixes #1502 2018-02-24 16:30:08 +09:00
shell Remove int64, uint64 typedefs in favor of int64_t / uint64_t. 2018-03-31 14:45:04 +07:00
smt Merge branch 'master' of https://github.com/z3prover/z3 2018-04-25 11:18:39 +02:00
solver Added tactic for QF_FPLRA 2018-04-24 12:43:11 +01:00
tactic Updated CMakelists.txt 2018-04-24 15:01:05 +01:00
test merge with pull request #1557 2018-04-07 17:22:49 -07:00
util fix #1592 #1587 2018-04-25 11:18:24 +02:00
CMakeLists.txt remove smtlib1 dependencies 2017-11-28 10:37:30 -08:00