Various improvements (#109)

* Bitwuzla: better const arrays handling

* Yices: Allow negative uninterpreted values

* Allow nested internalizer invocations

* Implement unsupported Bv operations

* Bitwuzla: fix Bv overflow checks

* Implement rewrites for Bv mul overflow checks

* Z3: Test bv overflow checks

* Yices: Test bv overflow checks

* Cvc: Test bv overflow checks

* Arith power eval

* fp.rem operation eval

* Disable random fp.rem expressions

* Rework random expr generator excludes

* fp.fma evaluator

* Comments on underflow/overflow

* Upgrade version to 0.5.3

Author: Saloed

README.md

@@ -9,9 +9,9 @@ Install via [Gradle](https://gradle.org/).
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.5.2")
+implementation("io.ksmt:ksmt-core:0.5.3")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.2")
+implementation("io.ksmt:ksmt-z3:0.5.3")
 ```
 
 ## Usage

buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts

@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.5.2"
+version = "0.5.3"
 
 repositories {
     mavenCentral()

docs/getting-started.md

@@ -17,17 +17,17 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.2")    
+    implementation("io.ksmt:ksmt-core:0.5.3")    
 }
 ```
 
 #### 3. Add one or more SMT solver dependencies:
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.2")
+    implementation("io.ksmt:ksmt-z3:0.5.3")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.2")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.3")
 }
 ```
 SMT solver specific packages are provided with solver native binaries. 

examples/build.gradle.kts

@@ -9,9 +9,9 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.2")
+    implementation("io.ksmt:ksmt-core:0.5.3")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.2")
+    implementation("io.ksmt:ksmt-z3:0.5.3")
 }
 
 java {