From af285d02c3ccf7c3c7f3f75e18ae56ae1857d5db Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Jun 2017 08:38:28 -0700 Subject: [PATCH] add documentation per #1058 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index dec8f34dd..93da0b2c7 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5350,6 +5350,7 @@ extern "C" { /** \brief Add a new formula \c a to the given goal. Conjunctions are split into separate formulas. + If the goal is \c false, adding new formulas is a no-op. If the formula \c a is \c true, then nothing is added. If the formula \c a is \c false, then the entire goal is replaced by the formula \c false.