Skip to content
Permalink
Browse files

Fix mathsat signature for BV_CONCAT

  • Loading branch information...
makaimann committed Jul 22, 2019
1 parent 9c0ec9a commit 5317bd5085d7446dcfbc1be9395bb49e6d12c7f8
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 5317bd5

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