From d12efb6097c07cbdb64487b99f376c995ec2ed49 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 19 May 2016 13:10:43 -0700
Subject: [PATCH] remove min/max, use qmax; disable cancellation during model
 evaluation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/arith/lia2card_tactic.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 7256d19c7..4c2e0dead 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -300,7 +300,7 @@ public:
     bool get_sum(expr* x, rational const& mul, expr_ref_vector& conds, expr_ref_vector& args, vector<rational>& coeffs, rational& coeff) {
         expr *y, *z, *u;
         rational r, q;
-		if (!is_app(x)) return false;
+        if (!is_app(x)) return false;
         app* f = to_app(x);
         bool ok = true;
         if (a.is_add(x)) {