mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Convert BVULT(X,Y) into !BVULE(Y,X)
Signed-off-by: Mikhail Ramalho <mikhail.ramalho@gmail.com>
This commit is contained in:
parent
41e0a12678
commit
c5336f8003
|
@ -25,7 +25,7 @@ Notes:
|
|||
#include "ast/fpa/fpa2bv_converter.h"
|
||||
#include "ast/rewriter/fpa_rewriter.h"
|
||||
|
||||
#define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); }
|
||||
#define BVULT(X,Y,R) { expr_ref t(m); t = m_bv_util.mk_ule(Y,X); m_simp.mk_not(t, R); }
|
||||
|
||||
fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
|
||||
m(m),
|
||||
|
|
Loading…
Reference in a new issue