Nikolaj Bjorner avatar Nikolaj Bjorner committed 8809681

some test cases for problem reported in stackoverflow

Signed-off-by: Nikolaj Bjorner <>;

Comments (0)

Files changed (2)


 #include "ast_pp.h"
 #include "reg_decl_plugins.h"
+static void check_equiv(ast_manager& m, expr* e1, expr* e2) {
+    front_end_params fp;
+    smt::solver solver(m, fp);
+    expr_ref equiv(m);
+    equiv = m.mk_not(m.mk_eq(e1,e2));
+    solver.assert_expr(equiv);
+    lbool is_sat = solver.check();
+    SASSERT(is_sat == l_false);
 static void simplify_formula(ast_manager& m, expr* e) {
     expr_ref result(m);
     expr_context_simplifier simp(m);
-          << mk_pp(e, m) << " |-> " 
+          << mk_pp(e, m) << "\n|->\n" 
           << mk_pp(result.get(), m) << "\n";);
+    check_equiv(m, e, result);
         "(benchmark samples :logic QF_LIA                         \n"
         " :extrafuns ((x Int) (y Int) (z Int) (u Int))            \n"
+        " :extrapreds ((p) (q) (r)) \n"
         " :formula (and (<= 1 x) (or (<= 1 x) (<= x y)))          \n"
         " :formula (and (<= 2 (ite (<= z 1) (ite (<= z 1) x y) (* 2 x))) (<= x y)) \n"
+        " :formula (or (and (not p) q (or (not r) (and (or (not p) q) r)))\
+                       (and (not p) q (or (and p (not q) r) (and (or (not p) q) (not r)))) \
+                       (and (or (and p (not q)) (and p q))\
+                            (or (and p q r) (and (or (not p) (not q)) (not r))))\
+                       (and (not p) (not q) (or (and (not p) q r) (and (or p (not q)) (not r))))\
+                       (and (not p) (not q) (or (not r) (and (or p (not q)) r))))\n"


     std::ostringstream buffer;
     buffer << "(benchmark presburger :status unknown :logic AUFLIA :extrapreds ((p1) (p2) (p3)) "
            << ":extrafuns ((a Int) (b Int))\n"
+           << ":extrapreds ((p) (q) (r))\n"
            << ":datatypes ((list (nil) (cons (hd Int) (tl list))))\n"
            << ":datatypes ((cell (cnil) (ccons (car cell) (cdr cell))))\n"
            << ":extrasorts (U)\n"
 void tst_quant_elim() {
+    test_formula(l_undef, "(exists ((p1 Bool) (q1 Bool) (r1 Bool))\
+                                    (and (or (not p1) (not q1) r1)\
+                                         (or (and (not p) (not q) (not p1) q1)\
+                                             (and (not p) q p1 (not q1))\
+                                             (and p (not q) p1 q1)\
+                                             (and p q p1 q1))\
+                                         (or (and (not r) (not r1))\
+                                             (and (= p p1) (= q q1) r r1)\
+                                             (and (not (and (= p p1) (= q q1))) (not (= r r1))))))");
     test_formula(l_false,"(forall (x Int) (y Int) (or (= x 0) (< (* 5 y) (* 6 x)) (> (* 5 y) (* 6 x))))");
     test_formula(l_false, "(forall (a Int) (b Int) (exists (x Int) (and (< a (* 20 x)) (< (* 20 x) b))))");
     test_formula(l_undef, "(exists (a Bool) (b Bool) (or (and p1 a) (and p2 (not b))))");
                  "(forall (x Int) (q1 Int) (q2 Int) (r1 Int) (r2 Int) "
                  "  (implies "
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.