From 9ca0faa0918c25656bda75c86e9df32b53e99d5b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Mar 2023 18:13:44 +0100 Subject: [PATCH] enable interactive example --- src/tactic/core/eliminate_predicates_tactic.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/core/eliminate_predicates_tactic.h b/src/tactic/core/eliminate_predicates_tactic.h index c2eb90742e1..51bb4a6c3c9 100644 --- a/src/tactic/core/eliminate_predicates_tactic.h +++ b/src/tactic/core/eliminate_predicates_tactic.h @@ -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)