z3py: Comment vérifier les informations de trace lors de l'utilisation de z3 python api

Question

Supposons que je souhaite vérifier les informations de trace de "random_split". J'ai écrit

enable_trace("random_split") 

dans mon script python qui utilise api python z3, mais rien ne montre.

Je me demande comment vérifier les informations de trace lors de l'utilisation de z3py?

Answer 1

Les traces ne sont disponibles qu'en mode débogage, vous devez donc compiler vous-même Z3 avec python scripts/mk_make.py --debug. Si la trace ne produit aucune sortie, alors ce morceau de code particulier n'est jamais atteint, donc il n'obtient jamais rien.