Skip to content
Permalink
Browse files

Merge pull request #598 from makaimann/msat-signature-fix

Fix mathsat signature for BV_CONCAT
  • Loading branch information...
mikand committed Jul 24, 2019
2 parents 9c0ec9a + 5317bd5 commit 09dc303185812149550110123ad266326beb1179
Showing with 6 additions and 1 deletion.
  1. +6 −1 pysmt/solvers/msat.py
@@ -464,7 +464,7 @@ def __init__(self, environment, msat_env):
mathsat.MSAT_TAG_BV_ADD: self._sig_binary,
mathsat.MSAT_TAG_BV_UDIV:self._sig_binary,
mathsat.MSAT_TAG_BV_UREM:self._sig_binary,
mathsat.MSAT_TAG_BV_CONCAT: self._sig_binary,
mathsat.MSAT_TAG_BV_CONCAT: self._sig_bv_concat,
mathsat.MSAT_TAG_BV_OR: self._sig_binary,
mathsat.MSAT_TAG_BV_XOR: self._sig_binary,
mathsat.MSAT_TAG_BV_AND: self._sig_binary,
@@ -565,6 +565,11 @@ def _sig_bv_extract(self, term, args):
t = self.env.stc.get_type(args[0])
return types.FunctionType(types.BVType(msb - lsb + 1), [t])

def _sig_bv_concat(self, term, args):
t1 = self.env.stc.get_type(args[0])
t2 = self.env.stc.get_type(args[1])
return types.FunctionType(types.BVType(t1.width + t2.width), [t1, t2])

def _sig_array_read(self, term, args):
t1 = self.env.stc.get_type(args[0])
t = t1.elem_type

0 comments on commit 09dc303

Please sign in to comment.
You can’t perform that action at this time.