1

I am using Z3 solver and adding and tracking specific assertions. I am carrying out my analysis in itterations. I was wondering if it is possible to remove one specific assertion and replace it with another?

Amir Ebrahimi
  • 115
  • 1
  • 10

1 Answers1

2

Yes, that is possible, but only indirectly, either via assumptions (which can be disabled later), or by using push/pop. See also the following posts and the links provided there:

Soft/Hard constraints in Z3

Incremental solving in Z3 using push command

What is the benifits of incremental solving?

Community
  • 1
  • 1
Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30