3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
z3/src
Nikolaj Bjorner 755b517001 fix #6600
ensure that semantics of last-indexof(t,"") = len(t)
2023-02-19 14:02:37 -08:00
..
ackermannization add doc for ackermannize 2022-12-27 12:02:08 -08:00
api track assumptions when parsing into a solver. This enables solver.from_file/solver.from_string to support assumptions/cores #6587 2023-02-14 11:09:11 -08:00
ast fix #6600 2023-02-19 14:02:37 -08:00
cmd_context track assumptions when parsing into a solver. This enables solver.from_file/solver.from_string to support assumptions/cores #6587 2023-02-14 11:09:11 -08:00
math fixes for #6590 2023-02-15 15:11:44 -08:00
model rename set-flat to set-flat-and-or to allow to differentiate parameters 2022-10-27 11:22:57 -07:00
muz clean up build warnings 2023-02-19 10:08:31 -08:00
nlsat fix bug in new core not detecting conflict, fix #6525, add tactic doc 2023-01-14 17:20:43 -05:00
opt experimental feature to access congruence closure of SimpleSolver 2022-12-30 21:41:27 -08:00
params don't flush stream when printing param vals 2023-01-03 09:35:17 +00:00
parsers Optimize calls to Z3_eval_smtlib2_string (#6422) 2022-10-28 13:57:22 -07:00
qe fix #6559 2023-02-04 13:33:40 -08:00
sat clean up build warnings 2023-02-19 10:08:31 -08:00
shell use setter method to easier track updates to settings. 2023-02-01 10:18:14 -08:00
smt fix #6591 2023-02-19 11:09:52 -08:00
solver fixes to mbqi in the new core based on #6575 2023-02-10 16:56:06 -08:00
tactic patch regressions 2023-02-12 20:12:01 -08:00
test compile warnings 2023-02-19 10:03:38 -08:00
util fix #6600 2023-02-19 14:02:37 -08:00
CMakeLists.txt create simplifier_solver wrapper to supply simplifier layer 2023-01-30 16:12:25 -08:00