From b797b345b549f66a4bccf925c9463c0fe40b8946 Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Wed, 5 Jun 2024 16:57:37 -0500
Subject: [PATCH] Handle non-linear terms gracefully in to_presburger

---
 src/qe/poly.ml                              |  5 ++++-
 src/qe/poly.mli                             |  2 ++
 src/qe/presburger.ml                        |  5 ++++-
 tests/regression/success/mult_two_polys.lus | 24 +++++++++++++++++++++
 4 files changed, 34 insertions(+), 2 deletions(-)
 create mode 100644 tests/regression/success/mult_two_polys.lus

diff --git a/src/qe/poly.ml b/src/qe/poly.ml
index d6a336486..102caa012 100644
--- a/src/qe/poly.ml
+++ b/src/qe/poly.ml
@@ -16,6 +16,8 @@
 
 *)
 
+exception Not_in_LIA
+
 type psummand = Numeral.t * (Var.t option)
 
 type poly = psummand list
@@ -370,7 +372,8 @@ let multiply_two_polys (pt1: poly) (pt2: poly) : poly =
     | _, [(i, None)] -> poly_times_num pt1 i
 
     | _ ->
-      failwith "Can only multiply two polys when at least one of them is constant."
+      (* failwith "Can only multiply two polys when at least one of them is constant." *)
+      raise Not_in_LIA
 
 (*
 (* Multiply up a list of presburger terms of at least one element. *)
diff --git a/src/qe/poly.mli b/src/qe/poly.mli
index 002855497..94805ebe9 100644
--- a/src/qe/poly.mli
+++ b/src/qe/poly.mli
@@ -23,6 +23,8 @@
     @author Ruoyu Zhang
 *)
 
+exception Not_in_LIA
+
 (** psummand is a constant or a variable with coefficient *)
 type psummand = Numeral.t * (Var.t option)
 
diff --git a/src/qe/presburger.ml b/src/qe/presburger.ml
index 0ab436c9b..646b6555f 100644
--- a/src/qe/presburger.ml
+++ b/src/qe/presburger.ml
@@ -88,7 +88,10 @@ let multiply_iformula_list (ifl: iformula list) : poly =
       List.fold_left 
         (fun accum e ->
           match accum, e with
-            | pl1, (Poly pl2) -> multiply_two_polys pl1 pl2
+            | pl1, (Poly pl2) -> (
+              try multiply_two_polys pl1 pl2
+              with Poly.Not_in_LIA -> raise Not_in_LIA
+            )
             | _ -> 
               failwith "multiply_iformula_list can only multiply polynomials.")
         pl 
diff --git a/tests/regression/success/mult_two_polys.lus b/tests/regression/success/mult_two_polys.lus
new file mode 100644
index 000000000..da58993a3
--- /dev/null
+++ b/tests/regression/success/mult_two_polys.lus
@@ -0,0 +1,24 @@
+node s2 (n: int) returns (x: int);
+var n0: int;
+let
+  n0 = n -> pre n0;
+  x = n0 -> pre x + n0;
+tel
+
+node s3 (n: int) returns (x: int);
+var mult: int;
+var n0: int;
+let
+  mult = 1 -> pre mult + 1;
+  n0 = n -> pre n0;
+  x = n0 * mult;
+tel
+
+node check_s3 (n: int) returns (x: bool);
+var x1: int;
+var x2: int;
+let 
+  x1 = s2(n);
+  x2 = s3(n);
+  check x1 = x2;
+tel
\ No newline at end of file