mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

enable interactive example

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-03-25 18:13:44 +01:00
parent 50bd6efea4
commit 9ca0faa091
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/core/eliminate_predicates_tactic.h
View file

@ -30,7 +30,7 @@ resolution.
the predicate `p` occurs once positively. All negative occurrences of `p` are resolved against this positive occurrence.
The result of resolution is a set of equalities between arguments to `p`. The function `f` is replaced by a partial solution.
```
```z3
(declare-fun f (Int Int Int) Int)
(declare-fun p (Int) Bool)
(declare-const a Int)