From e5716501e8f936100c2844242fdb1d2f9762da4f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 May 2015 19:47:00 -0700 Subject: [PATCH] add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/probe_arith.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/arith/probe_arith.h b/src/tactic/arith/probe_arith.h index ba95a2837..0ff64a0ba 100644 --- a/src/tactic/arith/probe_arith.h +++ b/src/tactic/arith/probe_arith.h @@ -66,6 +66,6 @@ probe * mk_is_qfufnra_probe(); ADD_PROBE("is-lia", "true if the goal is in LIA (linear integer arithmetic, formula may have quantifiers).", "mk_is_lia_probe()") ADD_PROBE("is-lra", "true if the goal is in LRA (linear real arithmetic, formula may have quantifiers).", "mk_is_lra_probe()") ADD_PROBE("is-lira", "true if the goal is in LIRA (linear integer and real arithmetic, formula may have quantifiers).", "mk_is_lira_probe()") - ADD_PROBE("is-qfufnra", "true if the goal is QF_UFNRA (quantifier-free nonlinear real arithmetic with other theories).", mk_is_qfufnra_probe()"); + ADD_PROBE("is-qfufnra", "true if the goal is QF_UFNRA (quantifier-free nonlinear real arithmetic with other theories).", "mk_is_qfufnra_probe()") */ #endif