mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove theory_card
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
0ff1b63307
commit
475072f5da
|
@ -351,7 +351,7 @@ namespace smt {
|
|||
// is available.
|
||||
if (!has_bv) {
|
||||
expr_ref tmp(m), fml(m);
|
||||
tmp = m.mk_fresh_const("card_proxy",m.mk_bool_sort());
|
||||
tmp = m.mk_fresh_const("pb_proxy",m.mk_bool_sort());
|
||||
fml = m.mk_iff(tmp, arg);
|
||||
ctx.internalize(fml, false);
|
||||
SASSERT(ctx.b_internalized(tmp));
|
||||
|
|
Loading…
Reference in a new issue