Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

infinite loop in modulo operation with variable divisor #7464

Open
amigalemming opened this issue Nov 24, 2024 · 1 comment
Open

infinite loop in modulo operation with variable divisor #7464

amigalemming opened this issue Nov 24, 2024 · 1 comment

Comments

@amigalemming
Copy link

I have the following Liquid Haskell code:

module Example.BinaryGCD where

import Prelude hiding (even)

{-@
even ::
   n : Integer ->
   {m : Bool | m = (n mod 2 = 0)}
@-}
even :: Integer -> Bool
even n = mod n 2 == 0

{-@
divTwoPow ::
   nn : {n : Integer | n>0} ->
   {m : Integer | m>0 && m mod 2 = 1 && m <= nn && nn mod m = 0}
@-}
divTwoPow :: Integer -> Integer
divTwoPow n =
   if even n then divTwoPow (div n 2) else n

The nn mod m = 0 part sends Z3 (version 4.8.12) to an infinite loop.
Here is the SMT code that Liquid Haskell extracts from the code above:

(set-option :auto-config false)
(set-option :model true)

(set-option :smt.mbqi false)

(define-sort Str () Int)
(declare-fun strLen (Str) Int)
(declare-fun subString (Str Int Int) Str)
(declare-fun concatString (Str Str) Str)
(define-sort Elt () Int)
(define-sort LSet () (Array Elt Bool))
(define-sort Map () (Array Elt Elt))
(define-fun smt_map_sel ((m Map) (k Elt)) Elt (select m k))
(define-fun smt_map_sto ((m Map) (k Elt) (v Elt)) Map (store m k v))
(define-fun smt_map_cup ((m1 Map) (m2 Map)) Map ((_ map (+ (Elt Elt) Elt)) m1 m2))
(define-fun smt_map_prj ((s LSet) (m Map)) Map ((_ map (ite (Bool Elt Elt) Elt)) s m ((as const (Array Elt Elt)) 0)))
(define-fun smt_map_to_set ((m Map)) LSet ((_ map (> (Elt Elt) Bool)) m ((as const (Array Elt Elt)) 0)))
(define-fun smt_map_max ((m1 Map) (m2 Map)) Map (lambda ((i Int)) (ite (> (select m1 i) (select m2 i)) (select m1 i) (select m2 i))))
(define-fun smt_map_min ((m1 Map) (m2 Map)) Map (lambda ((i Int)) (ite (< (select m1 i) (select m2 i)) (select m1 i) (select m2 i))))
(define-fun smt_map_shift ((n Int) (m Map)) Map (lambda ((i Int)) (select m (- i n))))
(define-fun smt_map_def ((v Elt)) Map ((as const (Map)) v))
(define-fun bool_to_int ((b Bool)) Int (ite b 1 0))
(define-fun Z3_OP_MUL ((x Int) (y Int)) Int (* x y))
(define-fun Z3_OP_DIV ((x Int) (y Int)) Int (div x y))
(declare-fun GHC.Internal.Float.log () Int)
(declare-fun GHC.Internal.Real.recip () Int)
(declare-fun GHC.Internal.Real.div () Int)
(declare-fun GHC.Types.LT () Int)
(declare-fun VV$35$$35$F$35$$35$10 () Int)
(declare-fun x_Tuple33 () Int)
(declare-fun x_Tuple22 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ () Int)
(declare-fun GHC.Internal.Real.rem () Int)
(declare-fun GHC.Classes.$124$$124$ () Int)
(declare-fun GHC.Classes.min () Int)
(declare-fun GHC.Internal.Data.Tuple.snd () Int)
(declare-fun GHC.Internal.Real.$36$W$58$$37$ () Int)
(declare-fun GHC.Num.Integer.$36$fEqInteger () Int)
(declare-fun GHC.Internal.Enum.C$58$Bounded () Int)
(declare-fun snd () Int)
(declare-fun x_Tuple21 () Int)
(declare-fun GHC.Internal.Base.. () Int)
(declare-fun GHC.Internal.Stack.Types.EmptyCallStack () Int)
(declare-fun GHC.Classes.$38$$38$ () Int)
(declare-fun GHC.Internal.Real.quotRem () Int)
(declare-fun VV$35$$35$F$35$$35$3 () Int)
(declare-fun GHC.Internal.Stack.Types.FreezeCallStack () Int)
(declare-fun VV$35$$35$F$35$$35$17 () Int)
(declare-fun len () Int)
(declare-fun VV$35$$35$F$35$$35$8 () Int)
(declare-fun GHC.Types.TrNameS () Int)
(declare-fun GHC.Classes.$61$$61$ () Int)
(declare-fun cast_as () Int)
(declare-fun Example.BinaryGCD.even () Int)
(declare-fun VV$35$$35$F$35$$35$12 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805059$35$$35$d2YP () Int)
(declare-fun GHC.Internal.Float.asinh () Int)
(declare-fun GHC.Classes.$62$ () Int)
(declare-fun GHC.Internal.Float.asin () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO () Bool)
(declare-fun lq_anf$36$$35$$35$7205759403792805052$35$$35$d2YI () Int)
(declare-fun GHC.Internal.Real.quot () Int)
(declare-fun GHC.Types.Module () Int)
(declare-fun GHC.Internal.Base.map () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR () Int)
(declare-fun fst () Int)
(declare-fun x_Tuple31 () Int)
(declare-fun papp2 () Int)
(declare-fun GHC.Internal.Num.abs () Int)
(declare-fun GHC.Num.Integer.IP () Int)
(declare-fun GHC.Internal.Real.$47$ () Int)
(declare-fun papp7 () Int)
(declare-fun papp1 () Int)
(declare-fun GHC.Internal.Float.sin () Int)
(declare-fun VV$35$$35$F$35$$35$2 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805063$35$$35$d2YT () Int)
(declare-fun GHC.Internal.Float.$42$$42$ () Int)
(declare-fun GHC.Classes.compare () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN () Bool)
(declare-fun lq_anf$36$$35$$35$7205759403792805056$35$$35$d2YM () Int)
(declare-fun papp5 () Int)
(declare-fun GHC.Num.Integer.IN () Int)
(declare-fun papp4 () Int)
(declare-fun GHC.Internal.Num.negate () Int)
(declare-fun GHC.Internal.Base.$36$ () Int)
(declare-fun GHC.Types.False () Bool)
(declare-fun GHC.Internal.Float.acos () Int)
(declare-fun GHC.Internal.Base.$43$$43$ () Int)
(declare-fun GHC.Types.TrNameD () Int)
(declare-fun lit$36$Example.BinaryGCD () Str)
(declare-fun lit$36$htam$45$liquid$45$0.0$45$inplace () Str)
(declare-fun totalityError () Int)
(declare-fun GHC.Classes.$47$$61$ () Int)
(declare-fun GHC.Internal.Float.tanh () Int)
(declare-fun GHC.Internal.Real.divMod () Int)
(declare-fun GHC.Internal.Float.cosh () Int)
(declare-fun GHC.Internal.Float.logBase () Int)
(declare-fun GHC.Internal.Maybe.Just () Int)
(declare-fun VV$35$$35$F$35$$35$6 () Int)
(declare-fun Example.BinaryGCD.divTwoPow () Int)
(declare-fun GHC.Tuple.$40$$44$$41$ () Int)
(declare-fun GHC.Internal.Real.$58$$37$ () Int)
(declare-fun GHC.Classes.max () Int)
(declare-fun GHC.Types.$91$$93$ () Int)
(declare-fun GHC.Classes.$60$$61$ () Int)
(declare-fun VV$35$$35$F$35$$35$4 () Int)
(declare-fun liquid_internal_this () Int)
(declare-fun VV$35$$35$F$35$$35$11 () Int)
(declare-fun GHC.Internal.Num.$45$ () Int)
(declare-fun GHC.Internal.Num.fromInteger () Int)
(declare-fun GHC.Classes.C$58$IP () Int)
(declare-fun VV$35$$35$F$35$$35$5 () Int)
(declare-fun GHC.Types.EQ () Int)
(declare-fun n$35$$35$a2XR () Int)
(declare-fun GHC.Internal.Float.cos () Int)
(declare-fun GHC.Internal.Float.acosh () Int)
(declare-fun GHC.Internal.Real.toInteger () Int)
(declare-fun GHC.Internal.Real.$36$fIntegralInteger () Int)
(declare-fun papp3 () Int)
(declare-fun GHC.Num.Integer.IS () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805055$35$$35$d2YL () Int)
(declare-fun autolen () Int)
(declare-fun GHC.Internal.Float.atan () Int)
(declare-fun GHC.Internal.IO.Exception.IOError () Int)
(declare-fun VV$35$$35$F$35$$35$9 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805065$35$$35$d2YV () Int)
(declare-fun GHC.Internal.Base.id () Int)
(declare-fun addrLen () Int)
(declare-fun GHC.Tuple.$40$$41$ () Int)
(declare-fun GHC.Internal.Float.exp () Int)
(declare-fun n$35$$35$a2XQ () Int)
(declare-fun GHC.Internal.Float.atanh () Int)
(declare-fun GHC.Types.True () Bool)
(declare-fun GHC.Internal.Err.error () Int)
(declare-fun GHC.Internal.Float.sinh () Int)
(declare-fun GHC.Classes.$60$ () Int)
(declare-fun head () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ () Int)
(declare-fun GHC.Internal.Float.tan () Int)
(declare-fun GHC.Internal.Real.$94$ () Int)
(declare-fun tail () Int)
(declare-fun GHC.Types.GT () Int)
(declare-fun GHC.Internal.Num.$42$ () Int)
(declare-fun VV$35$$35$F$35$$35$7 () Int)
(declare-fun GHC.Internal.Float.pi () Int)
(declare-fun GHC.Internal.Data.Either.Left () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Internal.Maybe.Just$35$$35$1 () Int)
(declare-fun papp6 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805054$35$$35$d2YK () Int)
(declare-fun GHC.Internal.Real.mod () Int)
(declare-fun GHC.Internal.Real.fromRational () Int)
(declare-fun GHC.Internal.Data.Tuple.fst () Int)
(declare-fun GHC.Internal.Num.$43$ () Int)
(declare-fun VV$35$$35$F$35$$35$14 () Bool)
(declare-fun GHC.Types.C$35$ () Int)
(declare-fun GHC.Internal.Stack.Types.PushCallStack () Int)
(declare-fun GHC.Internal.Float.sqrt () Int)
(declare-fun cast_as_int () Int)
(declare-fun GHC.Tuple.$40$$44$$44$$41$ () Int)
(declare-fun x_Tuple32 () Int)
(declare-fun GHC.Types.$58$ () Int)
(declare-fun GHC.Classes.$62$$61$ () Int)
(declare-fun GHC.Types.I$35$ () Int)
(declare-fun GHC.Classes.not () Int)
(declare-fun GHC.Internal.Real.fromIntegral () Int)
(declare-fun VV$35$$35$F$35$$35$13 () Int)
(declare-fun GHC.Internal.Maybe.Nothing () Int)
(declare-fun GHC.Internal.Data.Either.Right () Int)
(declare-fun apply$35$$35$4 (Int Int) (_ BitVec 32))
(declare-fun apply$35$$35$16 (Int Str) (_ BitVec 32))
(declare-fun apply$35$$35$32 (Int (_ BitVec 64)) Str)
(declare-fun apply$35$$35$10 (Int Bool) (_ BitVec 32))
(declare-fun apply$35$$35$8 (Int Bool) Str)
(declare-fun apply$35$$35$14 (Int Str) Str)
(declare-fun apply$35$$35$21 (Int (Array Int Bool)) (Array Int Bool))
(declare-fun apply$35$$35$27 (Int (_ BitVec 32)) (Array Int Bool))
(declare-fun apply$35$$35$0 (Int Int) Int)
(declare-fun apply$35$$35$25 (Int (_ BitVec 32)) Bool)
(declare-fun apply$35$$35$31 (Int (_ BitVec 64)) Bool)
(declare-fun apply$35$$35$1 (Int Int) Bool)
(declare-fun apply$35$$35$34 (Int (_ BitVec 64)) (_ BitVec 32))
(declare-fun apply$35$$35$13 (Int Str) Bool)
(declare-fun apply$35$$35$20 (Int (Array Int Bool)) Str)
(declare-fun apply$35$$35$11 (Int Bool) (_ BitVec 64))
(declare-fun apply$35$$35$5 (Int Int) (_ BitVec 64))
(declare-fun apply$35$$35$33 (Int (_ BitVec 64)) (Array Int Bool))
(declare-fun apply$35$$35$30 (Int (_ BitVec 64)) Int)
(declare-fun apply$35$$35$24 (Int (_ BitVec 32)) Int)
(declare-fun apply$35$$35$28 (Int (_ BitVec 32)) (_ BitVec 32))
(declare-fun apply$35$$35$23 (Int (Array Int Bool)) (_ BitVec 64))
(declare-fun apply$35$$35$26 (Int (_ BitVec 32)) Str)
(declare-fun apply$35$$35$12 (Int Str) Int)
(declare-fun apply$35$$35$7 (Int Bool) Bool)
(declare-fun apply$35$$35$17 (Int Str) (_ BitVec 64))
(declare-fun apply$35$$35$15 (Int Str) (Array Int Bool))
(declare-fun apply$35$$35$18 (Int (Array Int Bool)) Int)
(declare-fun apply$35$$35$6 (Int Bool) Int)
(declare-fun apply$35$$35$9 (Int Bool) (Array Int Bool))
(declare-fun apply$35$$35$3 (Int Int) (Array Int Bool))
(declare-fun apply$35$$35$29 (Int (_ BitVec 32)) (_ BitVec 64))
(declare-fun apply$35$$35$2 (Int Int) Str)
(declare-fun apply$35$$35$22 (Int (Array Int Bool)) (_ BitVec 32))
(declare-fun apply$35$$35$35 (Int (_ BitVec 64)) (_ BitVec 64))
(declare-fun apply$35$$35$19 (Int (Array Int Bool)) Bool)
(declare-fun coerce$35$$35$4 (Int) (_ BitVec 32))
(declare-fun coerce$35$$35$16 (Str) (_ BitVec 32))
(declare-fun coerce$35$$35$32 ((_ BitVec 64)) Str)
(declare-fun coerce$35$$35$10 (Bool) (_ BitVec 32))
(declare-fun coerce$35$$35$8 (Bool) Str)
(declare-fun coerce$35$$35$14 (Str) Str)
(declare-fun coerce$35$$35$21 ((Array Int Bool)) (Array Int Bool))
(declare-fun coerce$35$$35$27 ((_ BitVec 32)) (Array Int Bool))
(declare-fun coerce$35$$35$0 (Int) Int)
(declare-fun coerce$35$$35$25 ((_ BitVec 32)) Bool)
(declare-fun coerce$35$$35$31 ((_ BitVec 64)) Bool)
(declare-fun coerce$35$$35$1 (Int) Bool)
(declare-fun coerce$35$$35$34 ((_ BitVec 64)) (_ BitVec 32))
(declare-fun coerce$35$$35$13 (Str) Bool)
(declare-fun coerce$35$$35$20 ((Array Int Bool)) Str)
(declare-fun coerce$35$$35$11 (Bool) (_ BitVec 64))
(declare-fun coerce$35$$35$5 (Int) (_ BitVec 64))
(declare-fun coerce$35$$35$33 ((_ BitVec 64)) (Array Int Bool))
(declare-fun coerce$35$$35$30 ((_ BitVec 64)) Int)
(declare-fun coerce$35$$35$24 ((_ BitVec 32)) Int)
(declare-fun coerce$35$$35$28 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun coerce$35$$35$23 ((Array Int Bool)) (_ BitVec 64))
(declare-fun coerce$35$$35$26 ((_ BitVec 32)) Str)
(declare-fun coerce$35$$35$12 (Str) Int)
(declare-fun coerce$35$$35$7 (Bool) Bool)
(declare-fun coerce$35$$35$17 (Str) (_ BitVec 64))
(declare-fun coerce$35$$35$15 (Str) (Array Int Bool))
(declare-fun coerce$35$$35$18 ((Array Int Bool)) Int)
(declare-fun coerce$35$$35$6 (Bool) Int)
(declare-fun coerce$35$$35$9 (Bool) (Array Int Bool))
(declare-fun coerce$35$$35$3 (Int) (Array Int Bool))
(declare-fun coerce$35$$35$29 ((_ BitVec 32)) (_ BitVec 64))
(declare-fun coerce$35$$35$2 (Int) Str)
(declare-fun coerce$35$$35$22 ((Array Int Bool)) (_ BitVec 32))
(declare-fun coerce$35$$35$35 ((_ BitVec 64)) (_ BitVec 64))
(declare-fun coerce$35$$35$19 ((Array Int Bool)) Bool)
(declare-fun smt_lambda$35$$35$4 (Int (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$16 (Str (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$32 ((_ BitVec 64) Str) Int)
(declare-fun smt_lambda$35$$35$10 (Bool (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$8 (Bool Str) Int)
(declare-fun smt_lambda$35$$35$14 (Str Str) Int)
(declare-fun smt_lambda$35$$35$21 ((Array Int Bool) (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$27 ((_ BitVec 32) (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$0 (Int Int) Int)
(declare-fun smt_lambda$35$$35$25 ((_ BitVec 32) Bool) Int)
(declare-fun smt_lambda$35$$35$31 ((_ BitVec 64) Bool) Int)
(declare-fun smt_lambda$35$$35$1 (Int Bool) Int)
(declare-fun smt_lambda$35$$35$34 ((_ BitVec 64) (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$13 (Str Bool) Int)
(declare-fun smt_lambda$35$$35$20 ((Array Int Bool) Str) Int)
(declare-fun smt_lambda$35$$35$11 (Bool (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$5 (Int (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$33 ((_ BitVec 64) (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$30 ((_ BitVec 64) Int) Int)
(declare-fun smt_lambda$35$$35$24 ((_ BitVec 32) Int) Int)
(declare-fun smt_lambda$35$$35$28 ((_ BitVec 32) (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$23 ((Array Int Bool) (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$26 ((_ BitVec 32) Str) Int)
(declare-fun smt_lambda$35$$35$12 (Str Int) Int)
(declare-fun smt_lambda$35$$35$7 (Bool Bool) Int)
(declare-fun smt_lambda$35$$35$17 (Str (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$15 (Str (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$18 ((Array Int Bool) Int) Int)
(declare-fun smt_lambda$35$$35$6 (Bool Int) Int)
(declare-fun smt_lambda$35$$35$9 (Bool (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$3 (Int (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$29 ((_ BitVec 32) (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$2 (Int Str) Int)
(declare-fun smt_lambda$35$$35$22 ((Array Int Bool) (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$35 ((_ BitVec 64) (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$19 ((Array Int Bool) Bool) Int)
(declare-fun lam_arg$35$$35$1$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$2$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$3$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$4$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$5$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$6$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$7$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$1$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$2$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$3$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$4$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$5$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$6$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$7$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$1$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$2$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$3$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$4$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$5$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$6$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$7$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$1$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$2$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$3$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$4$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$5$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$6$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$7$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$1$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$2$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$3$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$4$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$5$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$6$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$7$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$1$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$2$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$3$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$4$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$5$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$6$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$7$35$$35$6 () Bool)
(assert (distinct GHC.Types.True GHC.Types.False))
(assert (distinct lit$36$htam$45$liquid$45$0.0$45$inplace lit$36$Example.BinaryGCD))


(assert (distinct GHC.Types.GT GHC.Types.EQ GHC.Types.LT))
(assert (= (strLen lit$36$Example.BinaryGCD) 17))
(assert (= (strLen lit$36$htam$45$liquid$45$0.0$45$inplace) 23))
(push 1)
(define-fun b$36$$35$$35$96 () Bool (and lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= (mod n$35$$35$a2XR 2) 0)) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN)))
(define-fun b$36$$35$$35$97 () Bool (= lq_anf$36$$35$$35$7205759403792805059$35$$35$d2YP 2))
(define-fun b$36$$35$$35$98 () Bool (= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ lq_anf$36$$35$$35$7205759403792805059$35$$35$d2YP))
(define-fun b$36$$35$$35$99 () Bool (and (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 0)) (>= lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR 0)) (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1)) (<= lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR n$35$$35$a2XR)) (=> (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1) (<= lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR n$35$$35$a2XR)) (=> (< 1 lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ) (< lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR n$35$$35$a2XR)) (= lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR (Z3_OP_DIV n$35$$35$a2XR lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ))))
(define-fun b$36$$35$$35$42 () Bool (not GHC.Types.False))
(define-fun b$36$$35$$35$107 () Bool (and (= (mod lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR VV$35$$35$F$35$$35$2) 0) (= (mod VV$35$$35$F$35$$35$2 2) 1) (> VV$35$$35$F$35$$35$2 0) (<= VV$35$$35$F$35$$35$2 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR)))
(define-fun b$36$$35$$35$108 () Bool (and (= (mod lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR VV$35$$35$F$35$$35$3) 0) (= (mod VV$35$$35$F$35$$35$3 2) 1) (> VV$35$$35$F$35$$35$3 0) (<= VV$35$$35$F$35$$35$3 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR)))
(define-fun b$36$$35$$35$109 () Bool (and (= (mod lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR VV$35$$35$F$35$$35$4) 0) (= (mod VV$35$$35$F$35$$35$4 2) 1) (> VV$35$$35$F$35$$35$4 0) (<= VV$35$$35$F$35$$35$4 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR)))
(define-fun b$36$$35$$35$110 () Bool (and (= (mod lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR VV$35$$35$F$35$$35$5) 0) (= (mod VV$35$$35$F$35$$35$5 2) 1) (> VV$35$$35$F$35$$35$5 0) (<= VV$35$$35$F$35$$35$5 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR)))
(define-fun b$36$$35$$35$111 () Bool (and (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 0)) (>= VV$35$$35$F$35$$35$6 0)) (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1)) (<= VV$35$$35$F$35$$35$6 n$35$$35$a2XR)) (=> (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1) (<= VV$35$$35$F$35$$35$6 n$35$$35$a2XR)) (=> (< 1 lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ) (< VV$35$$35$F$35$$35$6 n$35$$35$a2XR)) (= VV$35$$35$F$35$$35$6 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR) (= VV$35$$35$F$35$$35$6 (Z3_OP_DIV n$35$$35$a2XR lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ))))
(define-fun b$36$$35$$35$112 () Bool (and (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 0)) (>= VV$35$$35$F$35$$35$7 0)) (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1)) (<= VV$35$$35$F$35$$35$7 n$35$$35$a2XR)) (=> (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1) (<= VV$35$$35$F$35$$35$7 n$35$$35$a2XR)) (=> (< 1 lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ) (< VV$35$$35$F$35$$35$7 n$35$$35$a2XR)) (= VV$35$$35$F$35$$35$7 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR) (= VV$35$$35$F$35$$35$7 (Z3_OP_DIV n$35$$35$a2XR lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ))))
(define-fun b$36$$35$$35$113 () Bool (and (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 0)) (>= VV$35$$35$F$35$$35$8 0)) (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1)) (<= VV$35$$35$F$35$$35$8 n$35$$35$a2XR)) (=> (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1) (<= VV$35$$35$F$35$$35$8 n$35$$35$a2XR)) (=> (< 1 lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ) (< VV$35$$35$F$35$$35$8 n$35$$35$a2XR)) (= VV$35$$35$F$35$$35$8 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR) (= VV$35$$35$F$35$$35$8 (Z3_OP_DIV n$35$$35$a2XR lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ))))
(define-fun b$36$$35$$35$114 () Bool (and (= VV$35$$35$F$35$$35$9 lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ) (= VV$35$$35$F$35$$35$9 lq_anf$36$$35$$35$7205759403792805059$35$$35$d2YP)))
(define-fun b$36$$35$$35$83 () Bool (= lq_anf$36$$35$$35$7205759403792805052$35$$35$d2YI 2))
(define-fun b$36$$35$$35$115 () Bool (and (= VV$35$$35$F$35$$35$10 n$35$$35$a2XR) (> VV$35$$35$F$35$$35$10 0)))
(define-fun b$36$$35$$35$84 () Bool (= lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ lq_anf$36$$35$$35$7205759403792805052$35$$35$d2YI))
(define-fun b$36$$35$$35$116 () Bool (and (= VV$35$$35$F$35$$35$11 n$35$$35$a2XR) (> VV$35$$35$F$35$$35$11 0)))
(define-fun b$36$$35$$35$85 () Bool (and (=> (and (< 0 lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ) (<= 0 n$35$$35$a2XQ)) (and (< lq_anf$36$$35$$35$7205759403792805054$35$$35$d2YK lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ) (<= 0 lq_anf$36$$35$$35$7205759403792805054$35$$35$d2YK))) (= lq_anf$36$$35$$35$7205759403792805054$35$$35$d2YK (mod n$35$$35$a2XQ lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ))))
(define-fun b$36$$35$$35$117 () Bool (and (= VV$35$$35$F$35$$35$12 n$35$$35$a2XR) (> VV$35$$35$F$35$$35$12 0)))
(define-fun b$36$$35$$35$86 () Bool (= lq_anf$36$$35$$35$7205759403792805055$35$$35$d2YL 0))
(define-fun b$36$$35$$35$118 () Bool (and (= VV$35$$35$F$35$$35$13 n$35$$35$a2XR) (> VV$35$$35$F$35$$35$13 0)))
(define-fun b$36$$35$$35$87 () Bool (= lq_anf$36$$35$$35$7205759403792805056$35$$35$d2YM lq_anf$36$$35$$35$7205759403792805055$35$$35$d2YL))
(define-fun b$36$$35$$35$119 () Bool (= VV$35$$35$F$35$$35$14 (= lq_anf$36$$35$$35$7205759403792805054$35$$35$d2YK lq_anf$36$$35$$35$7205759403792805056$35$$35$d2YM)))
(define-fun b$36$$35$$35$120 () Bool (and (= VV$35$$35$F$35$$35$17 lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ) (= VV$35$$35$F$35$$35$17 lq_anf$36$$35$$35$7205759403792805052$35$$35$d2YI)))
(define-fun b$36$$35$$35$90 () Bool (> n$35$$35$a2XR 0))
(define-fun b$36$$35$$35$91 () Bool (= lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN (= (mod n$35$$35$a2XR 2) 0)))
(define-fun b$36$$35$$35$60 () Bool GHC.Types.True)
(define-fun b$36$$35$$35$92 () Bool (and (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= (mod n$35$$35$a2XR 2) 0)) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN)))
(define-fun b$36$$35$$35$93 () Bool (and (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= (mod n$35$$35$a2XR 2) 0)) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN)))
(define-fun b$36$$35$$35$94 () Bool (and (not lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= (mod n$35$$35$a2XR 2) 0)) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN)))
(define-fun b$36$$35$$35$95 () Bool (and (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= (mod n$35$$35$a2XR 2) 0)) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN)))
(push 1)
(push 1)
(assert (and true b$36$$35$$35$96 b$36$$35$$35$97 b$36$$35$$35$98 b$36$$35$$35$99 b$36$$35$$35$42 b$36$$35$$35$107 b$36$$35$$35$90 b$36$$35$$35$91 b$36$$35$$35$60 b$36$$35$$35$92 b$36$$35$$35$95))
(push 1)
(assert (not (= (mod VV$35$$35$F$35$$35$2 2) 1)))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and true b$36$$35$$35$96 b$36$$35$$35$97 b$36$$35$$35$98 b$36$$35$$35$99 b$36$$35$$35$42 b$36$$35$$35$108 b$36$$35$$35$90 b$36$$35$$35$91 b$36$$35$$35$60 b$36$$35$$35$92 b$36$$35$$35$95))
(push 1)
(assert (not (= (mod n$35$$35$a2XR VV$35$$35$F$35$$35$3) 0)))
(check-sat)
@amigalemming
Copy link
Author

Infinite loop also in z3-4.8.17.

The actual statement to be proved is the following, here expressed in Haskell/SBV:

SBV> prove $ \a b -> a.>0 .=> sMod a 2 .==0 .=> sMod b 2 ./= 0 .=> sMod (sDiv a 2) b .== 0 .=> sMod a b .== (0::SInteger)
^CInterrupted.

@amigalemming amigalemming mentioned this issue Nov 25, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@amigalemming