mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-07-15 22:26:18 -07:00
parent 6bd2a39fb7
commit ae55d30961
4 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/test/sls_test.cpp
View file

@ -55,6 +55,9 @@ namespace bv {
sls::context ctx(m, solver);
sls_terms terms(ctx);
sls_eval ev(terms, ctx);
for (auto e : es)
ev.register_term(e);
ev.init();
th_rewriter rw(m);
expr_ref r(e, m);
rw(r);
@ -171,6 +174,9 @@ namespace bv {
sls::context ctx(m, solver);
sls_terms terms(ctx);
sls_eval ev(terms, ctx);
for (auto e : es)
ev.register_term(e);
ev.init();
if (m.is_bool(e1)) {
SASSERT(m.is_true(r) || m.is_false(r));