From a07c6e479364099e9b09b1d68197b55f37d25930 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 1 May 2018 15:02:04 -0700
Subject: [PATCH] resolve

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/python/z3/z3.py | 14 +++-----------
 src/util/mpq.h          |  7 +++++++
 src/util/rational.h     |  6 ++++++
 3 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index fa8feb2fc..809e32644 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -8251,14 +8251,10 @@ def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
     ctx = _get_ctx(ctx)
     ssz, snames, ssorts = _dict2sarray(sorts, ctx)
     dsz, dnames, ddecls = _dict2darray(decls, ctx)
-<<<<<<< HEAD
-    return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
-=======
     try: 
-        return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
+        return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
     except Z3Exception as e:
         _handle_parse_error(e, ctx)
->>>>>>> fc719a5ee82361ffedb9ef46793e3401fdc32cc5
 
 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
     """Parse a file in SMT 2.0 format using the given sorts and decls.
@@ -8268,14 +8264,10 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
     ctx = _get_ctx(ctx)
     ssz, snames, ssorts = _dict2sarray(sorts, ctx)
     dsz, dnames, ddecls = _dict2darray(decls, ctx)
-<<<<<<< HEAD
-    return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
-=======
-    try: 
-        return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
+    try:
+        return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
     except Z3Exception as e:
         _handle_parse_error(e, ctx)
->>>>>>> fc719a5ee82361ffedb9ef46793e3401fdc32cc5
 
 def Interpolant(a,ctx=None):
     """Create an interpolation operator.
diff --git a/src/util/mpq.h b/src/util/mpq.h
index f1b261278..16b57237e 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -515,6 +515,13 @@ public:
         reset_denominator(c);
     }
 
+    void machine_idiv_rem(mpq const & a, mpq const & b, mpq & c, mpq & d) {
+        SASSERT(is_int(a) && is_int(b));
+        machine_div_rem(a.m_num, b.m_num, c.m_num, d.m_num);
+        reset_denominator(c);
+        reset_denominator(d);
+    }
+
     void machine_idiv(mpq const & a, mpq const & b, mpz & c) {
         SASSERT(is_int(a) && is_int(b));
         machine_div(a.m_num, b.m_num, c);
diff --git a/src/util/rational.h b/src/util/rational.h
index dc7b79419..644ca4342 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -189,6 +189,12 @@ public:
         return r;
     }
 
+    friend inline rational machine_div_rem(rational const & r1, rational const & r2, rational & rem) {
+        rational r;
+        rational::m().machine_idiv(r1.m_val, r2.m_val, r.m_val, rem.m_val);
+        return r;
+    }
+
     friend inline rational mod(rational const & r1, rational const & r2) {
         rational r;
         rational::m().mod(r1.m_val, r2.m_val, r.m_val);