From 8c5303a2dd6a25cae731e0500ad7e9acd07779de Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 22 Mar 2018 14:47:19 +0000
Subject: [PATCH] Use propt::l_set_to_{true,false}

Avoids the lower-level l_set_to(..., {true,false}) and may then
highlight opportunities for further optimisation.
---
 src/solvers/flattening/bv_pointers.cpp | 4 ++--
 src/solvers/flattening/bv_utils.cpp    | 8 +++-----
 2 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 9f47c211ab9..56a4e07fb21 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -768,7 +768,7 @@ void bv_pointerst::do_postponed(
       if(!is_dynamic)
         l2=!l2;
 
-      prop.l_set_to(prop.limplies(l1, l2), true);
+      prop.l_set_to_true(prop.limplies(l1, l2));
     }
   }
   else if(postponed.expr.id()==ID_object_size)
@@ -814,7 +814,7 @@ void bv_pointerst::do_postponed(
       literalt l1=bv_utils.equal(bv, saved_bv);
       literalt l2=bv_utils.equal(postponed.bv, size_bv);
 
-      prop.l_set_to(prop.limplies(l1, l2), true);
+      prop.l_set_to_true(prop.limplies(l1, l2));
     }
   }
   else
diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
index 87500ca48d5..441ca79e129 100644
--- a/src/solvers/flattening/bv_utils.cpp
+++ b/src/solvers/flattening/bv_utils.cpp
@@ -540,7 +540,7 @@ bvt bv_utilst::negate(const bvt &bv)
 
 bvt bv_utilst::negate_no_overflow(const bvt &bv)
 {
-  prop.l_set_to(overflow_negate(bv), false);
+  prop.l_set_to_false(overflow_negate(bv));
   return negate(bv);
 }
 
@@ -780,9 +780,7 @@ bvt bv_utilst::absolute_value(const bvt &bv)
 
 bvt bv_utilst::cond_negate_no_overflow(const bvt &bv, literalt cond)
 {
-  prop.l_set_to(
-    prop.limplies(cond, !overflow_negate(bv)),
-    true);
+  prop.l_set_to_true(prop.limplies(cond, !overflow_negate(bv)));
 
   return cond_negate(bv, cond);
 }
@@ -802,7 +800,7 @@ bvt bv_utilst::signed_multiplier_no_overflow(
 
   bvt result=unsigned_multiplier_no_overflow(neg0, neg1);
 
-  prop.l_set_to(result[result.size()-1], false);
+  prop.l_set_to_false(result[result.size() - 1]);
 
   literalt result_sign=prop.lxor(sign0, sign1);