fix: wrap -1 in sign built-in

tnelson · Aug 22, 2024 · 7b068ed · 7b068ed
1 parent 6b961d2
commit 7b068ed
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/forge/solver-specific/cvc5-tor.rkt b/forge/solver-specific/cvc5-tor.rkt
@@ -251,7 +251,7 @@
   ; Also declare Atom sort as the top level sort, and define various helper SMT functions.
 
   (define defined-funs (list
-     `(define-fun sign ((x__sign Int)) Int (ite (< x__sign 0) -1 (ite (> x__sign 0) 1 0)))
+     `(define-fun sign ((x__sign Int)) Int (ite (< x__sign 0) (- 1) (ite (> x__sign 0) 1 0)))
      `(define-fun reconcile-int_atom ((aset (Relation IntAtom))) IntAtom ((_ tuple.select 0) (set.choose aset)))
      `(assert (forall ((x1 IntAtom) (x2 IntAtom)) (=> (not (= x1 x2)) (not (= (IntAtom-to-Int x1) (IntAtom-to-Int x2))))))
      `(declare-fun univInt () (Relation IntAtom))