don't string match the produced interpolant -- it can change

SRI-CSL · Apr 6, 2023 · 1c8923f · 1c8923f
1 parent 10082b3
commit 1c8923f
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 11 deletions.
diff --git a/tests/regress/mcsat/nra/assumptions/issue261.smt2 b/tests/regress/mcsat/nra/assumptions/issue261.smt2
@@ -1984,4 +1984,4 @@ e1979
 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
 (check-sat-assuming-model (v0) ((/ (- 75) 58)))
-(get-unsat-model-interpolant)
+;;(get-unsat-model-interpolant)
diff --git a/tests/regress/mcsat/nra/assumptions/issue261.smt2.gold b/tests/regress/mcsat/nra/assumptions/issue261.smt2.gold
@@ -1,11 +1 @@
 unsat
-(or (< (+ -180841357257/2612 (* 444710031/2 (^ v0 2))) 0) (>= (* -1 (^ v0 2)) 0) (< (+ 2568250217007/5224 (* -1 v0)) 0) (= (^ v0 2) -1/27794700)
-    (>= (+ -1 (* -1 (^ v0 2))) 0) (>= (+ -3379123281/8 v0 (* -8906187/4 (^ v0 2))) 0) (>= (+ 222194717/3379123281 (* -2 (^ v0 2))) 0)
-    (>= (+ -162883/3379123281 (* -2 (^ v0 2))) 0) (< (+ -1/27794700 (* -1 v0)) 0) (= (^ v0 2) 222194717/3379123281) (= (^ v0 2) -6892) (< (^ v0 2) 0)
-    (= v0 104957259/1306) (= (^ v0 2) 180841357257/2612) (>= (+ -3379123281/8 v0) 0) (>= (+ 16152313/55589400 (* -3 (^ v0 2))) 0) (= (^ v0 2) 0)
-    (< (+ 6892 (* -1 (^ v0 2))) 0) (< (+ 1/27794700 (^ v0 2)) 0) (= (^ v0 2) -1/222357600) (= (^ v0 2) -1723/13516493124) (= (^ v0 2) 3379123281/16)
-    (>= (+ -3379123281/8 (* -1 (^ v0 2))) 0) (= (^ v0 2) 34985753/96798550081) (= (^ v0 2) -3446)
-    (>= (+ -22313794156579651/62614478572273800 (* -2 (^ v0 2))) 0) (< (+ -1/27794700 (* 3 (^ v0 2))) 0) (< (+ 18310751/34985753 (^ v0 2)) 0)
-    (< (+ -653/111178800 (* -1 v0)) 0) (>= (+ 1 (* -1 (^ v0 2))) 0) (< (+ 18310751/34985753 (* 3 (^ v0 2))) 0) (>= v0 0) (>= (+ -3379123281 (* 8 v0)) 0)
-    (>= (+ -180841357257 (* 2612 v0)) 0) (>= (+ -3379116389 (* 8 v0)) 0) (>= (+ -3379123281 (* 2612 (^ v0 2))) 0) (>= (+ 3446 (* -162883 (^ v0 2))) 0)
-    (>= (+ 162883 (* -6758246562 (^ v0 2))) 0) (>= (+ 16152313 (* -375686871433642800 (^ v0 2))) 0) (>= (+ 222194717 (* -751373742867285600 (^ v0 2))) 0))