From bf92e536882c87223a884d971e5d74197eaa208d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 30 Mar 2016 18:35:49 +0100 Subject: [PATCH] Annotation fix for pattern/quantifier probes --- src/tactic/probe.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/tactic/probe.h b/src/tactic/probe.h index 8894a75d8..a4754f8ed 100644 --- a/src/tactic/probe.h +++ b/src/tactic/probe.h @@ -89,14 +89,13 @@ probe * mk_produce_unsat_cores_probe(); ADD_PROBE("produce-proofs", "true if proof generation is enabled for the given goal.", "mk_produce_proofs_probe()") ADD_PROBE("produce-model", "true if model generation is enabled for the given goal.", "mk_produce_models_probe()") ADD_PROBE("produce-unsat-cores", "true if unsat-core generation is enabled for the given goal.", "mk_produce_unsat_cores_probe()") - ADD_PROBE("has-patterns", "true if the goal contains quantifiers with patterns.", "mk_has_pattern_probe()") */ probe * mk_has_quantifier_probe(); probe * mk_has_pattern_probe(); /* - ADD_PROBE("has-quantifier", "true if the goal contains quantifiers.", "mk_has_quantifier_probe()") + ADD_PROBE("has-quantifiers", "true if the goal contains quantifiers.", "mk_has_quantifier_probe()") ADD_PROBE("has-patterns", "true if the goal contains quantifiers with patterns.", "mk_has_pattern_probe()") */