missing number after #b

[m-fleury]

$ ./bach
Bitte nennen sind Sie erst die Anzahl an Bits, die Sie fuer den Exponenten und dann für die Mantisse verwenden wollen
128
24
sh: 1: z3: not found

$ ~/Documents/repos/bitwuzla/build/bin/bitwuzla ./code.smt2 
bitwuzla: ./code.smt2:172:35: expected '0' or '1' after '#b'

$ grep "\#b[^01]" code.smt2       
(assert (= expo_diff_long (concat #b expo_diff_2)))
(assert (= expo_diff_long_2 (concat #b expo_diff2_2)))

$ ~/.isabelle/contrib/cvc4-1.8/x86_64-linux/cvc4 code.smt2             
(error "Parse Error: code.smt2:172.36: Error finding next token.")

[Robin060500]

Den Fehler bekommt man leider, weil ich davon ausgegangen bin, das die Anzahl an Bits für den Exponenten immer kleiner ist, als die Anzahl an Bits für die Mantisse.

Sonst müsste ich in Zeile 172 nicht concat sondern extract verwenden.

Soll ich das ändern?

 

Robin 

   

Gesendet: Mittwoch, 01. Februar 2023 um 17:50 Uhr Von: "Mathias Fleury" @.> An: "Robin060500/Bachelorarbeit" @.> Cc: "Subscribed" @.***> Betreff: [Robin060500/Bachelorarbeit] missing number after #b (Issue #1)

 

$ ./bach

Bitte nennen sind Sie erst die Anzahl an Bits, die Sie fuer den Exponenten und dann für die Mantisse verwenden wollen

128

24

sh: 1: z3: not found

$ ~/Documents/repos/bitwuzla/build/bin/bitwuzla ./code.smt2

bitwuzla: ./code.smt2:172:35: expected '0' or '1' after '#b'

$ grep "#b[^01]" code.smt2

(assert (= expo_diff_long (concat #b expo_diff_2)))

(assert (= expo_diff_long_2 (concat #b expo_diff2_2)))

$ ~/.isabelle/contrib/cvc4-1.8/x86_64-linux/cvc4 code.smt2

(error "Parse Error: code.smt2:172.36: Error finding next token.")

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.Message ID: @.***>

[m-fleury]

If it easy to fix: fix it

If not: just document it by no producing an SMT file and producing an error message instead.

[Robin060500]

Ok I fixed it, hope it works now.