I would like to know is there any way to add some new constraints for existing declared variables in the solver without getting the model.
For example, if I have 2 declare functions:
(declare-fun k!648 () (_ BitVec 8)) (declare-fun k!647 () (_ BitVec 8)) and some constraint with it.
How can I get their declared names generally?
Aucun commentaire:
Enregistrer un commentaire