1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include "util/memory_manager.h"
8 #include "smt/params/smt_params.h"
9 #include "ast/ast.h"
10 #include "ast/arith_decl_plugin.h"
11 #include "ast/bv_decl_plugin.h"
12 #include "smt/smt_context.h"
13 #include "ast/reg_decl_plugins.h"
14
tst_check_assumptions()15 void tst_check_assumptions()
16 {
17 memory::initialize(0);
18 smt_params params;
19 ast_manager mgr;
20 reg_decl_plugins(mgr);
21
22 sort_ref b(mgr.mk_bool_sort(), mgr);
23 func_decl_ref pPred(mgr.mk_func_decl(symbol("p"), 0, static_cast<sort * const *>(nullptr), b), mgr);
24 func_decl_ref qPred(mgr.mk_func_decl(symbol("q"), 0, static_cast<sort * const *>(nullptr), b), mgr);
25 func_decl_ref rPred(mgr.mk_func_decl(symbol("r"), 0, static_cast<sort * const *>(nullptr), b), mgr);
26
27 app_ref p(mgr.mk_app(pPred,0,static_cast<expr * const *>(nullptr)), mgr);
28 app_ref q(mgr.mk_app(qPred,0,static_cast<expr * const *>(nullptr)), mgr);
29 app_ref r(mgr.mk_app(rPred,0,static_cast<expr * const *>(nullptr)), mgr);
30 app_ref pOqOr(mgr.mk_or(p,q,r), mgr);
31
32 app_ref np(mgr.mk_not(p), mgr);
33 app_ref nq(mgr.mk_not(q), mgr);
34 app_ref nr(mgr.mk_not(r), mgr);
35
36 smt::context ctx(mgr, params);
37 ctx.assert_expr(pOqOr);
38
39 expr * npE = np.get();
40 lbool res1 = ctx.check(1, &npE);
41 VERIFY(res1 == l_true);
42
43 ctx.assert_expr(npE);
44
45
46 expr * assumpt[] = { nq.get(), nr.get() };
47 //here it should crash
48 ctx.check(2, assumpt);
49 }
50
51