3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 14:32:06 +00:00

a few comments

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-08-02 10:31:10 -07:00
parent 385672ce5d
commit da159a9569

View file

@ -32,6 +32,8 @@ TODOs:
- support units of non-values (element variables).
Model construction would assign values to the elements.
- make unsat core tracking less naive by tracking dependencies at a finer grain.
- add statistics and use it from src/smt/seq_regex.cpp when extracting statistics from theory_seq.
- add selective tracing TRACE(seq, ..).